Documentation

LeanPool.Erdos97ConvexOctagon.CoverageCertificateFacts72

Bounded coverage-certificate computation facts #

source
theorem Erdos97Octagon.RawIncidence.StaticDirectCoverage.coverageBranchRoot_3_22 :
branchClaimRootValidB 3 22 (BranchClaim.patternThree 1) = true

Root audit for fixed branch (3, 22).

source
theorem Erdos97Octagon.RawIncidence.StaticDirectCoverage.coverageBranchNodes_5_34_00064 :
nodeClaimChunkValidB branchClaims5Row34 64 64 = true

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

source
theorem Erdos97Octagon.RawIncidence.StaticDirectCoverage.coverageBranchNodes_5_34_00128 :
nodeClaimChunkValidB branchClaims5Row34 128 64 = true

Node audit for fixed branch (5, 34), starting at 128.

source
theorem Erdos97Octagon.RawIncidence.StaticDirectCoverage.coverageBranchNodes_5_34_00192 :
nodeClaimChunkValidB branchClaims5Row34 192 64 = true

Node audit for fixed branch (5, 34), starting at 192.

source
theorem Erdos97Octagon.RawIncidence.StaticDirectCoverage.coverageBranchNodes_5_34_00256 :
nodeClaimChunkValidB branchClaims5Row34 256 64 = true

Node audit for fixed branch (5, 34), starting at 256.