Documentation

LeanPool.Erdos97ConvexOctagon.CoverageCertificateFacts86

Bounded coverage-certificate computation facts #

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

Root audit for fixed branch (4, 10).

source
theorem Erdos97Octagon.RawIncidence.StaticDirectCoverage.coverageBranchRoot_6_25 :
branchClaimRootValidB 6 25 (BranchClaim.search branchClaims6Row25) = true

Root audit for fixed branch (6, 25).

source
theorem Erdos97Octagon.RawIncidence.StaticDirectCoverage.coverageBranchNodes_6_25_00000 :
nodeClaimChunkValidB branchClaims6Row25 0 64 = true

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

source
theorem Erdos97Octagon.RawIncidence.StaticDirectCoverage.coverageBranchNodes_6_25_00064 :
nodeClaimChunkValidB branchClaims6Row25 64 64 = true

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

source
theorem Erdos97Octagon.RawIncidence.StaticDirectCoverage.coverageBranchNodes_6_25_00128 :
nodeClaimChunkValidB branchClaims6Row25 128 64 = true

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

source
theorem Erdos97Octagon.RawIncidence.StaticDirectCoverage.coverageBranchNodes_6_25_00192 :
nodeClaimChunkValidB branchClaims6Row25 192 19 = true

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