Bounded coverage-certificate computation facts

theorem Erdos97Octagon.RawIncidence.StaticDirectCoverage.coverageBranchRoot_0_32 : branchClaimRootValidB 0 32 (BranchClaim.patternTwo 0) = true

Root audit for fixed branch (0, 32).

theorem Erdos97Octagon.RawIncidence.StaticDirectCoverage.coverageBranchRoot_6_22 : branchClaimRootValidB 6 22 (BranchClaim.patternThree 1) = true

Root audit for fixed branch (6, 22).

theorem Erdos97Octagon.RawIncidence.StaticDirectCoverage.coverageBranchRoot_3_10 : branchClaimRootValidB 3 10 (BranchClaim.search branchClaims3Row10) = true

Root audit for fixed branch (3, 10).

theorem Erdos97Octagon.RawIncidence.StaticDirectCoverage.coverageBranchNodes_3_06_00064 : nodeClaimChunkValidB branchClaims3Row6 64 33 = true

Node audit for fixed branch (3, 6), starting at 64.

theorem Erdos97Octagon.RawIncidence.StaticDirectCoverage.coverageBranchNodes_3_10_00000 : nodeClaimChunkValidB branchClaims3Row10 0 64 = true

Node audit for fixed branch (3, 10), starting at 0.

theorem Erdos97Octagon.RawIncidence.StaticDirectCoverage.coverageBranchNodes_3_10_00064 : nodeClaimChunkValidB branchClaims3Row10 64 64 = true

Node audit for fixed branch (3, 10), starting at 64.

theorem Erdos97Octagon.RawIncidence.StaticDirectCoverage.coverageBranchNodes_3_10_00128 : nodeClaimChunkValidB branchClaims3Row10 128 17 = true

Node audit for fixed branch (3, 10), starting at 128.