pith. machine review for the scientific record. sign in
theorem proved term proof high

lm_above_threshold

show as:
view Lean formalization →

The declaration establishes that the language model alignment fraction exceeds one half. Researchers auditing Recognition Science validation certificates cite it to confirm the J-cost model meets the majority threshold on the language-model substrate. The proof is a one-line term-mode reduction that unfolds the rational definition and normalizes the comparison.

claimThe language model alignment fraction satisfies $7/8 > 1/2$.

background

The module ThreeSubstrateValidationCert supplies a Lean certificate for J-cost validations across language models, photonic qubits, and magnetized plasma. languageModelAlignmentFraction is defined as the rational 7/8, standing for the fraction of MLP layers in which J-cost beats cross-entropy. The module states that all three substrates share the fixed point at x=1 and the descent direction from the J-cost gradient.

proof idea

The term proof unfolds languageModelAlignmentFraction to the literal 7/8 and invokes norm_num to discharge the inequality 7/8 > 1/2.

why it matters in Recognition Science

The result anchors the language-model component of the ThreeSubstrateValidationCert, which the module presents as hypothesis-grade empirical support for J-cost uniqueness. It aligns with the Recognition Science landmarks of J-uniqueness (T5), the self-similar fixed point (T6), and the multi-channel J-cost extension. No downstream theorems yet consume it.

scope and limits

formal statement (Lean)

  47theorem lm_above_threshold : languageModelAlignmentFraction > 1/2 := by

proof body

Term-mode proof.

  48  unfold languageModelAlignmentFraction; norm_num
  49
  50/-- Photonic code rate: 7/8. -/

depends on (1)

Lean names referenced from this declaration's body.