Documentation

LeanPool.Erdos97ConvexOctagon.CoverageCertificateFacts43

Bounded coverage-certificate computation facts #

source
theorem Erdos97Octagon.RawIncidence.StaticDirectCoverage.coverageBranchRoot_1_14 :
branchClaimRootValidB 1 14 (BranchClaim.patternThree 178) = true

Root audit for fixed branch (1, 14).

source
theorem Erdos97Octagon.RawIncidence.StaticDirectCoverage.coverageBranchRoot_3_31 :
branchClaimRootValidB 3 31 (BranchClaim.search branchClaims3Row31) = true

Root audit for fixed branch (3, 31).

source
theorem Erdos97Octagon.RawIncidence.StaticDirectCoverage.coverageBranchNodes_3_30_00064 :
nodeClaimChunkValidB branchClaims3Row30 64 64 = true

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

source
theorem Erdos97Octagon.RawIncidence.StaticDirectCoverage.coverageBranchNodes_3_30_00128 :
nodeClaimChunkValidB branchClaims3Row30 128 64 = true

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

source
theorem Erdos97Octagon.RawIncidence.StaticDirectCoverage.coverageBranchNodes_3_30_00192 :
nodeClaimChunkValidB branchClaims3Row30 192 31 = true

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

source
theorem Erdos97Octagon.RawIncidence.StaticDirectCoverage.coverageBranchNodes_3_31_00000 :
nodeClaimChunkValidB branchClaims3Row31 0 64 = true

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