Bounded coverage-certificate computation facts

theorem Erdos97Octagon.RawIncidence.StaticDirectCoverage.coverageBranchRoot_0_09 : branchClaimRootValidB 0 9 (BranchClaim.patternTwo 0) = true

Root audit for fixed branch (0, 9).

theorem Erdos97Octagon.RawIncidence.StaticDirectCoverage.coverageBranchRoot_4_27 : branchClaimRootValidB 4 27 (BranchClaim.patternTwo 0) = true

Root audit for fixed branch (4, 27).

theorem Erdos97Octagon.RawIncidence.StaticDirectCoverage.coverageBranchRoot_1_31 : branchClaimRootValidB 1 31 (BranchClaim.search branchClaims1Row31) = true

Root audit for fixed branch (1, 31).

theorem Erdos97Octagon.RawIncidence.StaticDirectCoverage.coverageBranchNodes_1_30_00192 : nodeClaimChunkValidB branchClaims1Row30 192 64 = true

Node audit for fixed branch (1, 30), starting at 192.

theorem Erdos97Octagon.RawIncidence.StaticDirectCoverage.coverageBranchNodes_1_30_00256 : nodeClaimChunkValidB branchClaims1Row30 256 19 = true

Node audit for fixed branch (1, 30), starting at 256.

theorem Erdos97Octagon.RawIncidence.StaticDirectCoverage.coverageBranchNodes_1_31_00000 : nodeClaimChunkValidB branchClaims1Row31 0 64 = true

Node audit for fixed branch (1, 31), starting at 0.

theorem Erdos97Octagon.RawIncidence.StaticDirectCoverage.coverageBranchNodes_1_31_00064 : nodeClaimChunkValidB branchClaims1Row31 64 64 = true

Node audit for fixed branch (1, 31), starting at 64.