module module

`IndisputableMonolith.Foundation.ThreeSubstrateValidationCert`

show as: view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Cost module_import
IndisputableMonolith.Foundation.MultiChannelJCost module_import

declarations in this module (13)

inductive ValidationSubstrate L27
theorem validationSubstrateCount L31
theorem shared_fixed_point L34
theorem shared_descent L37
theorem shared_symmetry L41
def languageModelAlignmentFraction L45
theorem lm_fraction_eq L46
theorem lm_above_threshold L47
def photonicCodeRate L51
def photonic_code_rate_rfl L52
theorem seven_eighths_from_F2_cube L55
structure ThreeSubstrateCert L59
def threeSubstrateCert L68