Bounded coverage-certificate computation facts

theorem Erdos97Octagon.RawIncidence.StaticDirectCoverage.coverageBranchRoot_0_31 : branchClaimRootValidB 0 31 (BranchClaim.patternTwo 0) = true

Root audit for fixed branch (0, 31).

theorem Erdos97Octagon.RawIncidence.StaticDirectCoverage.coverageBranchRoot_6_21 : branchClaimRootValidB 6 21 (BranchClaim.patternThree 1) = true

Root audit for fixed branch (6, 21).

theorem Erdos97Octagon.RawIncidence.StaticDirectCoverage.coverageBranchRoot_3_05 : branchClaimRootValidB 3 5 (BranchClaim.search branchClaims3Row5) = true

Root audit for fixed branch (3, 5).

theorem Erdos97Octagon.RawIncidence.StaticDirectCoverage.coverageBranchRoot_3_06 : branchClaimRootValidB 3 6 (BranchClaim.search branchClaims3Row6) = true

Root audit for fixed branch (3, 6).

theorem Erdos97Octagon.RawIncidence.StaticDirectCoverage.coverageBranchNodes_3_04_00064 : nodeClaimChunkValidB branchClaims3Row4 64 50 = true

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

theorem Erdos97Octagon.RawIncidence.StaticDirectCoverage.coverageBranchNodes_3_05_00000 : nodeClaimChunkValidB branchClaims3Row5 0 64 = true

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

theorem Erdos97Octagon.RawIncidence.StaticDirectCoverage.coverageBranchNodes_3_05_00064 : nodeClaimChunkValidB branchClaims3Row5 64 52 = true

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

theorem Erdos97Octagon.RawIncidence.StaticDirectCoverage.coverageBranchNodes_3_06_00000 : nodeClaimChunkValidB branchClaims3Row6 0 64 = true

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