Bounded coverage-certificate computation facts

theorem Erdos97Octagon.RawIncidence.StaticDirectCoverage.coverageBranchRoot_0_33 : branchClaimRootValidB 0 33 (BranchClaim.patternTwo 0) = true

Root audit for fixed branch (0, 33).

theorem Erdos97Octagon.RawIncidence.StaticDirectCoverage.coverageBranchRoot_6_29 : branchClaimRootValidB 6 29 (BranchClaim.patternThree 6) = true

Root audit for fixed branch (6, 29).

theorem Erdos97Octagon.RawIncidence.StaticDirectCoverage.coverageBranchRoot_3_11 : branchClaimRootValidB 3 11 (BranchClaim.search branchClaims3Row11) = true

Root audit for fixed branch (3, 11).

theorem Erdos97Octagon.RawIncidence.StaticDirectCoverage.coverageBranchRoot_3_12 : branchClaimRootValidB 3 12 (BranchClaim.search branchClaims3Row12) = true

Root audit for fixed branch (3, 12).

theorem Erdos97Octagon.RawIncidence.StaticDirectCoverage.coverageBranchNodes_3_11_00000 : nodeClaimChunkValidB branchClaims3Row11 0 64 = true

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

theorem Erdos97Octagon.RawIncidence.StaticDirectCoverage.coverageBranchNodes_3_11_00064 : nodeClaimChunkValidB branchClaims3Row11 64 49 = true

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

theorem Erdos97Octagon.RawIncidence.StaticDirectCoverage.coverageBranchNodes_3_12_00000 : nodeClaimChunkValidB branchClaims3Row12 0 64 = true

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

theorem Erdos97Octagon.RawIncidence.StaticDirectCoverage.coverageBranchNodes_3_12_00064 : nodeClaimChunkValidB branchClaims3Row12 64 43 = true

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