Flat local checker for coverage certificates

structure Erdos97Octagon.RawIncidence.StaticDirectCoverage.NodeWordClaim : Type

Witness streams for one nonempty five-row word of a node claim.

• wordIndex : ℕ

  Index of the consecutive five-row word.

• rejectionTargets : List ℕ

  One semantic column-conflict target for every rejected row.

• patternOrigins : List ℕ

  Pattern origins for active rows covered by patterns.

• childIds : List ℕ

  Recursive child identifiers for active rows that continue the search.

• hardOrigins : List ℕ

  Exact hard origins for active rows at the final depth.

structure Erdos97Octagon.RawIncidence.StaticDirectCoverage.NodeClaim : Type

One postorder DFS node; child identifiers must point to earlier nodes.

• depth : ℕ

  Number of noncanonical search rows already assigned.

• code : UInt64

  Packed partial incidence table at this node.

• pairOnce : UInt64

  Pairs selected by at least one assigned row.

• pairTwice : UInt64

  Pairs selected by at least two assigned rows.

• conflictCoverId : ℕ

  Dense identifier of a globally audited repeated-pair row-mask cover.

• activeRows : UInt64

  Row indices whose pair and column guards both survive.

• rejectedRows : UInt64

  Pair-compatible row indices rejected by the semantic column guard.

• patternRows : UInt64

  Legal-row indices stopped by pattern origins.

• wordClaims : Array NodeWordClaim

  Nonempty witness streams, grouped by consecutive five-row words.

structure Erdos97Octagon.RawIncidence.StaticDirectCoverage.BranchClaims : Type

Flat postorder claims for one fixed branch.

• nodeGroups : Array (Array NodeClaim)

  Every locally checked node in shallow 64-entry groups, children before parents.

• nodeCount : ℕ

  Total number of nodes across all groups.

• rootId : ℕ

  Identifier of the branch root.

inductive Erdos97Octagon.RawIncidence.StaticDirectCoverage.BranchClaim : Type

A fixed branch closes immediately by a pattern, or by a flat search certificate.

• patternTwo (patternIdentifier : ℕ) : BranchClaim

  A pattern covers the first two fixed rows.

• patternThree (patternIdentifier : ℕ) : BranchClaim

  A pattern covers all three fixed rows.

• search (claims : BranchClaims) : BranchClaim

  The five remaining rows are covered by postorder local claims.

def Erdos97Octagon.RawIncidence.StaticDirectCoverage.NodeClaim.wordAt (claim : NodeClaim) (wordIndex : ℕ) : NodeWordClaim

Retrieve one of at most seven sparse word claims, defaulting to empty streams.

Equations

• claim.wordAt wordIndex = Erdos97Octagon.RawIncidence.StaticDirectCoverage.nodeWordClaimAtAux✝ claim.wordClaims wordIndex 0 7

def Erdos97Octagon.RawIncidence.StaticDirectCoverage.BranchClaims.nodeAt (claims : BranchClaims) (identifier : ℕ) : NodeClaim

Retrieve one node without unfolding an entire large flat array literal.

Equations

• claims.nodeAt identifier = (claims.nodeGroups.getD (identifier / 64) #[]).getD (identifier % 64) Erdos97Octagon.RawIncidence.StaticDirectCoverage.defaultNodeClaim✝

def Erdos97Octagon.RawIncidence.StaticDirectCoverage.rowFromCode (code : UInt64) (centre : Vertex) : UInt64

Read one row byte from a packed incidence-table code.

Equations

• Erdos97Octagon.RawIncidence.StaticDirectCoverage.rowFromCode code centre = code >>> UInt64.ofNat (8 * ↑centre) &&& 255

def Erdos97Octagon.RawIncidence.StaticDirectCoverage.assignedCentres (depth : ℕ) : List Vertex

Assigned centres at one search depth.

Equations

• Erdos97Octagon.RawIncidence.StaticDirectCoverage.assignedCentres depth = [0, 1, 2] ++ List.take depth Erdos97Octagon.RawIncidence.searchCentres

def Erdos97Octagon.RawIncidence.StaticDirectCoverage.assignmentsFromCode (code : UInt64) (depth : ℕ) : List RowAssignment

Reconstruct the semantic assignment prefix from a code and search depth.

Equations

• One or more equations did not get rendered due to their size.

def Erdos97Octagon.RawIncidence.StaticDirectCoverage.pairStateFromAssignments (assignments : List RowAssignment) : PairState

Reconstruct the packed pair state from the semantic assignment prefix.

Equations

• One or more equations did not get rendered due to their size.

def Erdos97Octagon.RawIncidence.StaticDirectCoverage.columnStateFromAssignments (assignments : List RowAssignment) : ColumnState

Reconstruct the packed column state from the semantic assignment prefix.

Equations

• One or more equations did not get rendered due to their size.

def Erdos97Octagon.RawIncidence.StaticDirectCoverage.densePatternSummaryLookup (identifier : ℕ) : Option PatternSummary

Constant-depth lookup of one compact pattern-summary identifier.

Equations

• One or more equations did not get rendered due to their size.

def Erdos97Octagon.RawIncidence.StaticDirectCoverage.denseHardSummaryLookup (identifier : ℕ) : Option HardSummary

Constant-depth lookup of one compact exact-summary identifier.

Equations

• One or more equations did not get rendered due to their size.

def Erdos97Octagon.RawIncidence.StaticDirectCoverage.patternIdentifierPackedMatchesB (identifier : ℕ) (code : UInt64) : Bool

Packed-only pattern-summary validation for the first computation gate.

Equations

• One or more equations did not get rendered due to their size.

def Erdos97Octagon.RawIncidence.StaticDirectCoverage.hardIdentifierPackedMatchesB (identifier : ℕ) (code : UInt64) : Bool

Packed-only exact-summary validation for the first computation gate.

Equations

• One or more equations did not get rendered due to their size.

def Erdos97Octagon.RawIncidence.StaticDirectCoverage.rowIndexWord (rows : UInt64) (offset : ℕ) : List ℕ

Selected row indices in one fixed five-index word.

Equations

• One or more equations did not get rendered due to their size.

def Erdos97Octagon.RawIncidence.StaticDirectCoverage.conflictCoverLookup (identifier : ℕ) : Option ConflictCover

Retrieve one conflict cover without unfolding the full generated table.

Equations

• One or more equations did not get rendered due to their size.

def Erdos97Octagon.RawIncidence.StaticDirectCoverage.NodeRowValid (claims : BranchClaims) (identifier : ℕ) (claim : NodeClaim) (centre : Vertex) (remaining : List Vertex) (pairState : PairState) (index : ℕ) : Prop

Semantic consequence recorded for one active legal-row index.

Equations

• One or more equations did not get rendered due to their size.

def Erdos97Octagon.RawIncidence.StaticDirectCoverage.nodeWordValidB (claims : BranchClaims) (identifier : ℕ) (claim : NodeClaim) (centre : Vertex) (remaining : List Vertex) (pairState : PairState) (wordIndex : ℕ) : Bool

Validate one of the seven disjoint five-row words of a node claim.

Equations

• One or more equations did not get rendered due to their size.

theorem Erdos97Octagon.RawIncidence.StaticDirectCoverage.nodeRowValid_of_word (claims : BranchClaims) (identifier : ℕ) (claim : NodeClaim) (centre : Vertex) (remaining : List Vertex) (pairState : PairState) (wordIndex index : ℕ) (hword : nodeWordValidB claims identifier claim centre remaining pairState wordIndex = true) (hindex : index ∈ rowIndexWord claim.activeRows (5 * wordIndex)) : NodeRowValid claims identifier claim centre remaining pairState index

Every active index accepted by one compact word has its recorded outcome.

def Erdos97Octagon.RawIncidence.StaticDirectCoverage.rejectedRowValidB (claim : NodeClaim) (centre : Vertex) (remaining : List Vertex) (index target : ℕ) : Bool

Validate one semantically rejected row of a node claim.

Equations

• One or more equations did not get rendered due to their size.

def Erdos97Octagon.RawIncidence.StaticDirectCoverage.rejectedWordValidB (claim : NodeClaim) (centre : Vertex) (remaining : List Vertex) (indices targets : List ℕ) : Bool

Validate at most five rejected rows using one semantic conflict each.

Equations

• One or more equations did not get rendered due to their size.

def Erdos97Octagon.RawIncidence.StaticDirectCoverage.RejectedRowValid (claim : NodeClaim) (centre : Vertex) (remaining : List Vertex) (index : ℕ) : Prop

Semantic column-conflict consequence recorded for one rejected row.

Equations

• One or more equations did not get rendered due to their size.

theorem Erdos97Octagon.RawIncidence.StaticDirectCoverage.rejectedRowValid_of_word (claim : NodeClaim) (centre : Vertex) (remaining : List Vertex) (indices targets : List ℕ) (index : ℕ) (hword : rejectedWordValidB claim centre remaining indices targets = true) (hindex : index ∈ indices) : RejectedRowValid claim centre remaining index

Every rejected index accepted by one compact word has a semantic conflict.

def Erdos97Octagon.RawIncidence.StaticDirectCoverage.nodePruningValidB (claims : BranchClaims) (identifier : ℕ) : Bool

Validate the conservative pair/column row partition of one node.

Equations

• One or more equations did not get rendered due to their size.

def Erdos97Octagon.RawIncidence.StaticDirectCoverage.nodeTransitionsValidB (claims : BranchClaims) (identifier : ℕ) : Bool

Validate the active row outcomes and child-state transitions of one node.

Equations

• One or more equations did not get rendered due to their size.

def Erdos97Octagon.RawIncidence.StaticDirectCoverage.nodeLocalValidB (claims : BranchClaims) (identifier : ℕ) : Bool

Fail-closed local validation of one postorder node.

Equations

• One or more equations did not get rendered due to their size.

def Erdos97Octagon.RawIncidence.StaticDirectCoverage.nodeClaimChunkValidB (claims : BranchClaims) (start count : ℕ) : Bool

Validate a bounded consecutive chunk of postorder node identifiers.

Equations

• One or more equations did not get rendered due to their size.

def Erdos97Octagon.RawIncidence.StaticDirectCoverage.BranchClaims.LocallyValid (claims : BranchClaims) : Prop

Every node in a flat branch passes its local checker.

Equations

• claims.LocallyValid = ∀ identifier < claims.nodeCount, Erdos97Octagon.RawIncidence.StaticDirectCoverage.nodeLocalValidB claims identifier = true

theorem Erdos97Octagon.RawIncidence.StaticDirectCoverage.nodeLocalValid_of_chunk {claims : BranchClaims} {start count identifier : ℕ} (haudit : nodeClaimChunkValidB claims start count = true) (hlower : start ≤ identifier) (hupper : identifier < start + count) : nodeLocalValidB claims identifier = true

Extract one local node fact from a bounded chunk audit.

def Erdos97Octagon.RawIncidence.StaticDirectCoverage.nodePruningChunkValidB (claims : BranchClaims) (start count : ℕ) : Bool

Validate only row-partition facts in a bounded node chunk.

Equations

• One or more equations did not get rendered due to their size.

def Erdos97Octagon.RawIncidence.StaticDirectCoverage.nodeTransitionsChunkValidB (claims : BranchClaims) (start count : ℕ) : Bool

Validate only active transitions in a bounded node chunk.

Equations

• One or more equations did not get rendered due to their size.

def Erdos97Octagon.RawIncidence.StaticDirectCoverage.allNodeClaimsValidB (claims : BranchClaims) : Bool

Validate all postorder claims in bounded 64-node blocks.

Equations

• One or more equations did not get rendered due to their size.

def Erdos97Octagon.RawIncidence.StaticDirectCoverage.searchBranchRootValidB (orbit : Fin 7) (rowTwo : Fin 35) (claims : BranchClaims) : Bool

Validate the exact fixed-row root carried by one search claim array.

Equations

• One or more equations did not get rendered due to their size.

def Erdos97Octagon.RawIncidence.StaticDirectCoverage.branchClaimRootValidB (orbit : Fin 7) (rowTwo : Fin 35) (claim : BranchClaim) : Bool

Validate the immediate pattern or exact fixed-row state of one branch claim.

Equations

• One or more equations did not get rendered due to their size.