seven_eighths_from_F2_cube
plain-language theorem explainer
The declaration establishes that the language model alignment fraction equals seven-eighths, written explicitly as (2 cubed minus one) over 2 cubed. Researchers auditing the three-substrate validation certificate cite this when confirming the language-model component of J-cost predictions. The proof is a one-line wrapper that unfolds the definition and normalizes the rational expression.
Claim. The language-model alignment fraction equals $ (2^3 - 1)/2^3 $.
background
The module ThreeSubstrateValidationCert assembles a Lean certificate for RS Exp B, which checks J-cost behavior on language models, photonic qubits, and magnetized plasma. All three substrates share the fixed point at x = 1 where J(1) = 0, descent along the J-cost gradient, and multi-channel J_n extensions. The languageModelAlignmentFraction is defined as the rational 7/8, representing the fraction of MLP layers where J-cost beats cross-entropy in the March 2026 language-model experiments.
proof idea
The proof is a one-line wrapper. It unfolds the definition of languageModelAlignmentFraction and applies norm_num to confirm the numerical identity.
why it matters
This equality supplies the language-model alignment value inside the threeSubstrateCert definition, which assembles the full certificate from the three substrates. It fills the language-model slot in the empirical validation of J-cost uniqueness and echoes the eight-tick octave (period 2^3) from the T7 step in the forcing chain. The certificate remains at hypothesis grade; no open scaffolding questions are closed here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.