Bind statement: formalized to a recorded statement_hash

[Deicyde]

Status: obsolete-base draft; do not merge or mechanically retarget. The durable review-bundle direction now lives in #75 under tracker #49. Preserve this PR’s proof-invariant statement-meaning requirement there after #156 and the #140 replacements, with mandatory versioned enforcement. This head’s opt-in hash can be deleted to bypass verification and should be closed once the requirement is confirmed in the replacement.

Historical note: this was drafted as one commit on #115. That base closed unmerged; preserve the design record here and rebuild the unique work as described above.

This fixes H5 from the #115 contract audit, a gap that already exists on main.

What was wrong

statement: formalized was not tied to anything it certified. Skeleton's review_hash was printed but stored in no frontmatter and compared by nothing. A type edit that still compiled, or an edit to the article's statement text that left the frontmatter alone, therefore kept the article fully proved.

Changes

• An article may record statement_hash: sha256:<64 lowercase hex> beside statement: formalized. The loader checks the format and rejects the key with statement: retracted, without statement: formalized, or with mathlib: true.
• autoform skeleton prints each article's hash: == ID · statement_hash sha256:... in text, and statement_hash in JSON. The hash is SHA-256 over canonical JSON of three things:
  • the schema name, autoform-statement/v1;
  • the published statement text: the body between the title and the first heading, with dependency sections dropped and line endings and trailing whitespace normalized;
  • the sorted, de-duplicated name, kind, and elaborated meaning of every lean: declaration and every project declaration its statement rests on.
• A theorem's meaning is its type, so a proof leaves the hash alone. Axioms, external assumptions, boundary modules, the Lean version, and the cited passage are left out.
• autoform skeleton --check-statements compares every recorded hash with the current one. It exits 1 with one line per drifted article: error: ID: statement_hash OLD is recorded but the statement now hashes to NEW; re-review the statement and record the new hash.
• The check also fails an article that records a hash but has no lean:, or whose names do not all resolve. When no article records a hash, it prints no article records statement_hash; nothing to check and exits 0 without running Lean.
• autoform-verify.yml runs the check after the kernel-trust audit.
• The skeleton report schema moves to autoform-skeleton/v5 to carry the hashed statement text.
• The skills follow the key:
  • Formalize records the hash when it records statement: formalized.
  • Agent Review reports it when a statement passes.
  • Roadmap and the revision contract remove it wherever they remove statement: formalized. That includes the fallback for an AUTOFORM_REF that predates statement: retracted.

Tests

New in tests/test_graph.py:

• test_records_a_statement_hash
• test_rejects_a_statement_hash_without_a_statement_to_bind

New in tests/test_skeleton.py:

• test_statement_hash_binds_the_statement_text_and_meaning_only
• test_article_statement_is_the_published_statement_with_normalized_line_ends
• test_report_records_the_statement_text_its_hash_binds
• test_cli_check_statements_skips_lean_when_no_article_records_a_hash
• test_cli_check_statements_fails_on_a_changed_statement
• test_cli_check_statements_fails_when_a_recorded_hash_cannot_be_computed
• test_cli_check_statements_sets_the_probe_timeout
• test_statement_hash_survives_a_proof_and_catches_a_type_edit, which runs against real Lean

Local runs at f3725f9:

• ruff check autoform_cli servers tests: clean.
• Real Lean (AUTOFORM_REQUIRE_REAL_LEAN_TESTS=1), the CI skeleton step's selection, tests/test_skeleton.py plus tests/test_project_inspect.py::test_stale_inherited_mathlib_is_ignored_by_real_lake: 170 passed.
• Real Lean (AUTOFORM_REQUIRE_REAL_LEAN_TESTS=1), tests/test_lake_artifact_audit.py tests/test_impact.py tests/test_contract.py: 136 passed, 1 skipped. The skip is test_helper_runs_on_python_310, because python3.10 is not installed on this machine.
• Full suite without Lean: 1269 passed, 46 skipped, 4 failed. The 4 failures are the tests/test_scaffold.py pin tests. They fail only because my local clone has no origin remote, so plugin_pin() finds no pin. In a clone with origin they pass (63 of 63), and they pass in CI.

Caveats

• Recording is opt-in. Articles without statement_hash are not checked, so an existing project gets no protection until it records hashes.
• A v4 report written by an older --output no longer loads; regenerate it.
• --check-statements does not combine with --node, --json, --output, --packets, or --passages, so it always checks the whole blueprint.
• HTML comments inside the statement text are hashed. Editing one rotates the hash even though the published page does not change.
• A project whose AUTOFORM_REF predates the key stops at autoform check with unsupported frontmatter key 'statement_hash'. Move the pin and take the new workflow before recording hashes.
• A toolchain bump rotates hashes when it changes the elaborated terms.
• This is a drift check, not reviewer authentication: anyone who can edit the frontmatter can record a new hash. Whether workers are trusted is still an open decision (D4 in the contract audit), and this PR changes no governance.

[Deicyde]

This is not ready to restack or merge yet. The exact-head audit found five contract blockers:

1. The hash is not proof-invariant. The probe seeds trusted from proof axioms, and statement_hash hashes that whole closure. A theorem proved through a local axiom can lose a local definition from the hash when only its proof changes. Emit/hash a separate statement-meaning closure and add the real-Lean regression.
2. Enforcement is removable: deleting statement_hash while retaining statement: formalized makes --check-statements succeed. Make binding mandatory through a durable project policy (or for every applicable formalized statement), rather than checking only hashes that remain present.
3. Changing frontmatter declaration: theorem to def preserves the hash but changes status semantics so a stated item can become fully proved without proof review. Bind or validate the authored classification against the Lean declaration kind.
4. This must follow fixed Deploy Pages only after autoform verify passes, and refuse a lean: name defined twice #140. Without Pages waiting for successful verify, a drifted commit can fail the new check and still deploy. The example also pins c994d83, whose CLI lacks --check-statements, so the generated workflow currently fails even when no hashes exist.
5. Runtime omits the new authored assertion. On the cleaned Add opt-in open statements and conditional proof status #138 base, project it and bump the runtime schema (v3→v4) with exact-schema tests.

Also settle whether v1 binds the published H1 and imported-definition semantics, add a fixed golden digest, avoid shifting graph.Node positional fields, and make all-unresolved text output match the documented statement_hash none contract.

Please replay the unique commit onto the valid integration stack after #139/#140; do not retain the closed #115 ancestry.