Documentation

LeanPool.Erdos97ConvexOctagon.CoverageCertificateFacts68

Bounded coverage-certificate computation facts #

source
theorem Erdos97Octagon.RawIncidence.StaticDirectCoverage.coverageBranchRoot_3_18 :
branchClaimRootValidB 3 18 (BranchClaim.patternThree 5) = true

Root audit for fixed branch (3, 18).

source
theorem Erdos97Octagon.RawIncidence.StaticDirectCoverage.coverageBranchNodes_5_31_00192 :
nodeClaimChunkValidB branchClaims5Row31 192 64 = true

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

source
theorem Erdos97Octagon.RawIncidence.StaticDirectCoverage.coverageBranchNodes_5_31_00256 :
nodeClaimChunkValidB branchClaims5Row31 256 64 = true

Node audit for fixed branch (5, 31), starting at 256.

source
theorem Erdos97Octagon.RawIncidence.StaticDirectCoverage.coverageBranchNodes_5_31_00320 :
nodeClaimChunkValidB branchClaims5Row31 320 32 = true

Node audit for fixed branch (5, 31), starting at 320.

source
theorem Erdos97Octagon.RawIncidence.StaticDirectCoverage.coverageBranchNodes_5_31_00352 :
nodeClaimChunkValidB branchClaims5Row31 352 32 = true

Node audit for fixed branch (5, 31), starting at 352.