Documentation

LeanPool.Erdos97ConvexOctagon.CoverageCertificateFacts77

Bounded coverage-certificate computation facts #

source
theorem Erdos97Octagon.RawIncidence.StaticDirectCoverage.coverageBranchRoot_4_01 :
branchClaimRootValidB 4 1 (BranchClaim.patternTwo 0) = true

Root audit for fixed branch (4, 1).

source
theorem Erdos97Octagon.RawIncidence.StaticDirectCoverage.coverageBranchRoot_6_10 :
branchClaimRootValidB 6 10 (BranchClaim.search branchClaims6Row10) = true

Root audit for fixed branch (6, 10).

source
theorem Erdos97Octagon.RawIncidence.StaticDirectCoverage.coverageBranchNodes_6_09_00064 :
nodeClaimChunkValidB branchClaims6Row9 64 51 = true

Node audit for fixed branch (6, 9), starting at 64.

source
theorem Erdos97Octagon.RawIncidence.StaticDirectCoverage.coverageBranchNodes_6_10_00000 :
nodeClaimChunkValidB branchClaims6Row10 0 64 = true

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

source
theorem Erdos97Octagon.RawIncidence.StaticDirectCoverage.coverageBranchNodes_6_10_00064 :
nodeClaimChunkValidB branchClaims6Row10 64 64 = true

Node audit for fixed branch (6, 10), starting at 64.

source
theorem Erdos97Octagon.RawIncidence.StaticDirectCoverage.coverageBranchNodes_6_10_00128 :
nodeClaimChunkValidB branchClaims6Row10 128 30 = true

Node audit for fixed branch (6, 10), starting at 128.