Commit 8670ae9
committed
gate-2: characteristic theorem family audit, revision 4
Audit the Gate 2 nominees against the falsifier in
roadmap-gates.adoc - naturally echo-shaped, not reducible to
generic sigma or fiber lemmas. Verdict: 4-of-4 surviving.
Roadmap amendments:
Withdraw EchoCharacteristic.visible-constraint, reduces to
proj_2; retained as expository.
Withdraw EchoIntegration.knowledge-and-controlled-degradation,
a literal product of two facts over disjoint frameworks.
Nominate EchoGraded.degrade-via-join, categorical join law.
Name EchoGraded.degrade-compose explicitly.
Add EchoChoreo.applyChoreo-compose, role-reachability transport.
Add EchoLinear.degradeMode-compose, linearity-mode weakening.
New construction closes EI-1:
RoleGraded introduces RoleGEcho : Role -> Grade -> Set with
two independent actions and a commuting-square theorem
choreo-grade-commute. Both decoration witnesses appear on both
sides; satisfies the same-data test.
Honest qualification: of choreo-grade-commute 18 cases,
exactly one carries non-trivial content. EI-1 closure is
protocol-correct but substantively narrow. The follow-up
question is tracked as EI-2 and closed in commit 7.1 parent f68b6d6 commit 8670ae9
6 files changed
Lines changed: 1370 additions & 5 deletions
File tree
- docs
- proofs/agda/characteristic
0 commit comments