Documentation

LeanPool.Erdos97ConvexOctagon.CoverageCertificateFacts79

Bounded coverage-certificate computation facts #

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

Root audit for fixed branch (4, 3).

source
theorem Erdos97Octagon.RawIncidence.StaticDirectCoverage.coverageBranchRoot_6_13 :
branchClaimRootValidB 6 13 (BranchClaim.search branchClaims6Row13) = true

Root audit for fixed branch (6, 13).

source
theorem Erdos97Octagon.RawIncidence.StaticDirectCoverage.coverageBranchNodes_6_12_00064 :
nodeClaimChunkValidB branchClaims6Row12 64 61 = true

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

source
theorem Erdos97Octagon.RawIncidence.StaticDirectCoverage.coverageBranchNodes_6_13_00000 :
nodeClaimChunkValidB branchClaims6Row13 0 64 = true

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

source
theorem Erdos97Octagon.RawIncidence.StaticDirectCoverage.coverageBranchNodes_6_13_00064 :
nodeClaimChunkValidB branchClaims6Row13 64 64 = true

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

source
theorem Erdos97Octagon.RawIncidence.StaticDirectCoverage.coverageBranchNodes_6_13_00128 :
nodeClaimChunkValidB branchClaims6Row13 128 5 = true

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