Documentation

LeanPool.Erdos97ConvexOctagon.CoverageCertificateFacts51

Bounded coverage-certificate computation facts #

source
theorem Erdos97Octagon.RawIncidence.StaticDirectCoverage.coverageBranchRoot_2_00 :
branchClaimRootValidB 2 0 (BranchClaim.patternThree 1) = true

Root audit for fixed branch (2, 0).

source
theorem Erdos97Octagon.RawIncidence.StaticDirectCoverage.coverageBranchRoot_5_14 :
branchClaimRootValidB 5 14 (BranchClaim.search branchClaims5Row14) = true

Root audit for fixed branch (5, 14).

source
theorem Erdos97Octagon.RawIncidence.StaticDirectCoverage.coverageBranchNodes_5_12_00064 :
nodeClaimChunkValidB branchClaims5Row12 64 64 = true

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

source
theorem Erdos97Octagon.RawIncidence.StaticDirectCoverage.coverageBranchNodes_5_12_00128 :
nodeClaimChunkValidB branchClaims5Row12 128 64 = true

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

source
theorem Erdos97Octagon.RawIncidence.StaticDirectCoverage.coverageBranchNodes_5_12_00192 :
nodeClaimChunkValidB branchClaims5Row12 192 10 = true

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

source
theorem Erdos97Octagon.RawIncidence.StaticDirectCoverage.coverageBranchNodes_5_14_00000 :
nodeClaimChunkValidB branchClaims5Row14 0 64 = true

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