Documentation

LeanPool.Erdos97ConvexOctagon.CoverageCertificateFacts92

Bounded coverage-certificate computation facts #

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

Root audit for fixed branch (4, 16).

source
theorem Erdos97Octagon.RawIncidence.StaticDirectCoverage.coverageBranchRoot_6_32 :
branchClaimRootValidB 6 32 (BranchClaim.search branchClaims6Row32) = true

Root audit for fixed branch (6, 32).

source
theorem Erdos97Octagon.RawIncidence.StaticDirectCoverage.coverageBranchNodes_6_31_00192 :
nodeClaimChunkValidB branchClaims6Row31 192 29 = true

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

source
theorem Erdos97Octagon.RawIncidence.StaticDirectCoverage.coverageBranchNodes_6_31_00221 :
nodeClaimChunkValidB branchClaims6Row31 221 29 = true

Node audit for fixed branch (6, 31), starting at 221.

source
theorem Erdos97Octagon.RawIncidence.StaticDirectCoverage.coverageBranchNodes_6_32_00000 :
nodeClaimChunkValidB branchClaims6Row32 0 64 = true

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

source
theorem Erdos97Octagon.RawIncidence.StaticDirectCoverage.coverageBranchNodes_6_32_00064 :
nodeClaimChunkValidB branchClaims6Row32 64 64 = true

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