Item 13: Scaffolding self-verification
Infrastructure · difficulty entry · project none · open · node item-13
— satisfied, kept open
Satisfied by the scaffolding rounds and kept open. The Lean chain compiles and audits, and the house harness, the registries and the CI job that runs them are exercised end to end by smoke.faf-asymp-refl, smoke.chain-compiles and simplex.rational-points-sum-to-one. It stays filed because the registry's demand rule means every entry answers an item, including these, and because a future change to the harness reopens exactly this question. Record: projects/normativity/CLAIMS.md; checkers/.
Registered results bearing on this item
- simplex.rational-points-sum-to-one: A worked example of the schema, not a research result: the house enumeration checker generates the 28 rational simplex points at denominator six and confirms each sums to one. It exists so the registr
- smoke.chain-compiles: States a Mathlib limit in the dependency's own vocabulary, so it typechecks only if both halves of the chain agree.
- smoke.faf-asymp-refl: Reaches a real declaration in the pinned dependency. Certifies the chain, not mathematics.
Where it hangs
- held by enabling-work