Soundness of the exhaustive coverage-certificate manifest #
theorem
Erdos97Octagon.RawIncidence.StaticDirectCoverage.coverageBranchClaim_search_locallyValid
{orbit : Fin 7}
{rowTwo : Fin 35}
{claims : BranchClaims}
(hclaim : coverageBranchClaim orbit rowTwo = BranchClaim.search claims)
:
claims.LocallyValid
Every search claim selected by the complete manifest has all local node audits.
Semantic validity accessors for every generated certificate table.
theorem
Erdos97Octagon.RawIncidence.StaticDirectCoverage.branchClaim_impossible
(audits : CertificateAudits)
{p : Vertex → Plane}
{Q : OctagonIncidence}
(hC : ConvexIndependent ℝ p)
(hR : Realises p Q)
(hN : Q.Normalized)
(hSparse : Q.PairSparse)
(hBalanced : Q.Balanced)
(orbit : Fin 7)
(hrowOne : Q.targets 1 = packedRow (canonicalRowMask orbit))
(rowTwo : Fin 35)
(hrowTwo : Q.targets 2 = packedRow (rowTwoMask rowTwo))
(claim : BranchClaim)
(hroot : branchClaimRootValidB orbit rowTwo claim = true)
(hlocally : ∀ (claims : BranchClaims), claim = BranchClaim.search claims → claims.LocallyValid)
:
A root-audited branch claim and its local search audits contradict the corresponding realised fixed-row branch.
theorem
Erdos97Octagon.RawIncidence.StaticDirectCoverage.coverageBranchClaim_impossible
{p : Vertex → Plane}
{Q : OctagonIncidence}
(hC : ConvexIndependent ℝ p)
(hR : Realises p Q)
(hN : Q.Normalized)
(hSparse : Q.PairSparse)
(hBalanced : Q.Balanced)
(orbit : Fin 7)
(hrowOne : Q.targets 1 = packedRow (canonicalRowMask orbit))
(rowTwo : Fin 35)
(hrowTwo : Q.targets 2 = packedRow (rowTwoMask rowTwo))
:
The generated claim for one fixed canonical branch is semantically impossible.
theorem
Erdos97Octagon.RawIncidence.coverageCanonicalBranch_impossible
{p : Vertex → Plane}
{Q : OctagonIncidence}
(hC : ConvexIndependent ℝ p)
(hR : Realises p Q)
(hN : Q.Normalized)
(hSparse : Q.PairSparse)
(hBalanced : Q.Balanced)
(rowOneIndex : Fin 7)
(hrowOne : Q.targets 1 = packedRow (canonicalRowMask rowOneIndex))
:
The exhaustive flat certificate excludes every normalized branch with a canonical first row.