Documentation

LeanPool.Erdos97ConvexOctagon.CoverageCertificateFacts81

Bounded coverage-certificate computation facts #

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

Root audit for fixed branch (4, 5).

source
theorem Erdos97Octagon.RawIncidence.StaticDirectCoverage.coverageBranchRoot_6_16 :
branchClaimRootValidB 6 16 (BranchClaim.search branchClaims6Row16) = true

Root audit for fixed branch (6, 16).

source
theorem Erdos97Octagon.RawIncidence.StaticDirectCoverage.coverageBranchNodes_6_15_00064 :
nodeClaimChunkValidB branchClaims6Row15 64 64 = true

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

source
theorem Erdos97Octagon.RawIncidence.StaticDirectCoverage.coverageBranchNodes_6_15_00128 :
nodeClaimChunkValidB branchClaims6Row15 128 64 = true

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

source
theorem Erdos97Octagon.RawIncidence.StaticDirectCoverage.coverageBranchNodes_6_15_00192 :
nodeClaimChunkValidB branchClaims6Row15 192 9 = true

Node audit for fixed branch (6, 15), starting at 192.

source
theorem Erdos97Octagon.RawIncidence.StaticDirectCoverage.coverageBranchNodes_6_16_00000 :
nodeClaimChunkValidB branchClaims6Row16 0 64 = true

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