Documentation

LeanPool.Erdos97ConvexOctagon.CoverageCertificateFacts88

Bounded coverage-certificate computation facts #

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

Root audit for fixed branch (4, 12).

source
theorem Erdos97Octagon.RawIncidence.StaticDirectCoverage.coverageBranchRoot_6_27 :
branchClaimRootValidB 6 27 (BranchClaim.search branchClaims6Row27) = true

Root audit for fixed branch (6, 27).

source
theorem Erdos97Octagon.RawIncidence.StaticDirectCoverage.coverageBranchNodes_6_27_00000 :
nodeClaimChunkValidB branchClaims6Row27 0 64 = true

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

source
theorem Erdos97Octagon.RawIncidence.StaticDirectCoverage.coverageBranchNodes_6_27_00064 :
nodeClaimChunkValidB branchClaims6Row27 64 64 = true

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

source
theorem Erdos97Octagon.RawIncidence.StaticDirectCoverage.coverageBranchNodes_6_27_00128 :
nodeClaimChunkValidB branchClaims6Row27 128 64 = true

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

source
theorem Erdos97Octagon.RawIncidence.StaticDirectCoverage.coverageBranchNodes_6_27_00192 :
nodeClaimChunkValidB branchClaims6Row27 192 32 = true

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