From 8f6c73959c687d423b5a6e21a1a0cf2530fcf949 Mon Sep 17 00:00:00 2001
From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com>
Date: Sat, 19 Sep 2026 19:33:45 +0000
Subject: [PATCH] chore(governance): stop declaring repository identity in
 settings.yml

probot/settings applies this file on every push to the default branch, so `name`,
`description`, `homepage` and `private` here are instructions, not documentation. The estate has
already paid for that: the template carried `name: "{{REPO}}"`, GitHub collapsed the illegal braces
to dashes, the repo renamed itself to `-REPO-` on every push and its old URL 404'd.

This file now matches the template's own header and rule, with the four identity keys removed and
everything else left as it was. Repository identity and visibility are set out of band, once, by
the owner. Enforced by scripts/check-no-placeholders.sh.
---
 .github/settings.yml | 63 +++++++++++++++++++++++++++++++++++++++++---
 1 file changed, 59 insertions(+), 4 deletions(-)

diff --git a/.github/settings.yml b/.github/settings.yml
index ab1b6987..094206a2 100644
--- a/.github/settings.yml
+++ b/.github/settings.yml
@@ -6,14 +6,46 @@
 # This file defines repository-level configuration that is automatically
 # applied by the probot/settings app when changes are pushed to the default
 # branch. Install the app at: https://github.com/apps/settings
+#
+# ─── THIS FILE MUST NEVER DECLARE REPOSITORY IDENTITY ─────────────────────────
+#
+# It carries NO `name`, `description`, `homepage` or `private` key, and it must
+# never gain one. The reason is a real incident, not a hypothetical:
+#
+#   This file previously read `name: "{{REPO}}"`. probot/settings applies it on
+#   every push to the default branch, so it submitted the literal string
+#   `{{REPO}}` as the repository name. GitHub sanitises an invalid name by
+#   collapsing each run of illegal characters to a dash — `{{REPO}}` became
+#   `-REPO-`. The template renamed itself on every push, its old URL 404'd, and
+#   it was mistaken for a deleted repository. `description` was likewise left
+#   reading the literal `{{DESCRIPTION}}` on the live repo.
+#
+# Two properties make identity keys unsafe here specifically:
+#
+#   1. This is a TEMPLATE. `just repo-init` fills placeholders in repos minted by the
+#      scaffolder — but GitHub's "Use this template" button copies the default
+#      branch verbatim and never runs `just repo-init`. Any placeholder left in a
+#      probot-managed file therefore reaches children unrendered.
+#   2. Identity is not shareable. The template must be public while children
+#      default private; a child cannot inherit either `name` or `private` from
+#      its parent without being wrong.
+#
+# Repository identity and visibility are therefore set OUT OF BAND: once per
+# repo, at creation time, by the operator (the Configure stage of ADR-0003).
+# `just repo-init` deliberately runs NO `gh` commands — it prints the exact
+# `gh repo edit` commands as next steps instead. Fail-closed default: repos
+# stay private unless the owner flips visibility deliberately; the template's
+# own name and visibility are set deliberately by the owner.
+#
+# Everything below is safe to inherit: it is true of every RSR repo regardless
+# of that repo's name, purpose or visibility.
+#
+# Enforced by `scripts/check-no-placeholders.sh`, which fails if this file
+# contains a `{{` token or declares any of the four identity keys.
 
 # ─── Repository Settings ───────────────────────────────────────────────────────
 
 repository:
-  name: "proven"
-  description: "Formally verified safety via Idris2 dependent types — mathematically proven safe operations that cannot crash"
-  homepage: "https://github.com/hyperpolymath/proven"
-  private: false
   has_issues: true
   has_projects: true
   has_wiki: false
@@ -103,3 +135,26 @@ labels:
 
 # ─── Branch Protection ─────────────────────────────────────────────────────────
 
+# A required context must name a check that is actually EMITTED, or the branch
+# deadlocks: the check never reports, so it stays permanently pending, and with
+# enforce_admins even the owner cannot merge or push. This block previously
+# required three contexts, two of which no repo has ever emitted —
+#
+#   "codeql"       is emitted as `analyze (actions, none)`  (job id + matrix)
+#   "hypatia-scan" is emitted as `scan / Hypatia Neurosymbolic Analysis`
+#                  (a reusable-workflow call always reports `caller / called`)
+#
+# — while "openssf-compliance" resolved only because its job *id* is literally
+# `openssf-compliance` and it declares no `name:` and no matrix. That is the
+# rule: pin the job **id** to the context string. Note this file is applied by
+# probot on every push to the default branch, so a wrong context here does not
+# merely describe protection, it re-imposes the deadlock on every push.
+#
+# `contexts` is deliberately EMPTY rather than aspirational. Requiring a check
+# that cannot pass is the same defect as requiring one that cannot report, and
+# on this repo no check can currently run at all: GitHub Actions is billing-
+# blocked for PRIVATE repositories on this account ("The job was not started
+# because recent account payments have failed or your spending limit needs to be
+# increased"), which is why every workflow here fails with zero steps while the
+# estate's public repos run normally. Repopulate this list — one context at a
+# time, each pinned to a job id, each verified green — once Actions can run.