Masses Dof Pricing Base Coefficient Two Of Minimal

The base coefficient

The declaration base_coefficient_two_of_minimal establishes a specific fact about how degrees of freedom are priced in the Recognition Science framework. It shows that if a pricing rule assigns the same integer rung unit to each degree of freedom, requires at least one rung per degree, and is minimal among all such nondegenerate rules, then that unit must be 1 and a channel with two sides prices at exactly 2 rungs. The argument is a short derivation in the machine-checked library of formal results, built from the definition of the pricing structure and the minimality condition.

The framework models a degree of freedom as a configuration choice that contributes an integer number of rungs to a particle's mass ladder position. Independent degrees of freedom add their exponents, so the only freedom in the whole pricing rule is this single integer per degree. The minimality principle selects the smallest such integer, and the derivation shows that integer is 1. A channel, which is one distinction with exactly two sides, therefore carries exponent 2, and the base coefficient in the mass formula becomes 2.

This result does not claim that the minimality principle itself is proved. It is a modeling choice, a selection principle, not a proven statement. The result only shows what follows if minimality is assumed. Without that assumption, a second nondegenerate unit exists, namely 2, and it changes the coherence quantum observably, so the base coefficient is not forced by the pricing structure alone.

/-- **THEOREM (the base coefficient recovered).** Under the minimal pricing,
a channel's two-sided dof count (premise P2: one channel is one distinction,
and a distinction has exactly two sides, `Foundation/BoolFromLogic.lean`)
prices at 2 rungs. -/
theorem base_coefficient_two_of_minimal (p : DofPricing)
    (hmin : ∀ q : DofPricing, p.rungPerDof ≤ q.rungPerDof) :
    p.exponentOf 2 = 2 := by
  have hu := DofPricing.unit_eq_one_of_minimal p hmin
  simp [DofPricing.exponentOf, hu]

/-- A per-dof rung pricing: each configuration degree of freedom contributes
the same INTEGER rung unit (integrality banked by the ℤ-ladder; homogeneity is
the modeling content of "degree of freedom"), at least one rung
(nondegeneracy: a genuine dof is visible in the price, the same exclusion
`UnitFromMinimality` applies to the zero exponent). Independent dofs add
exponents by `dof_exponents_add`, so the only freedom in the rule is this one
integer. -/
structure DofPricing where
  rungPerDof : ℤ
  rungPerDof_pos : 1 ≤ rungPerDof

/-- **THEOREM (the boundary, packaged).** Without the minimality principle:
a second nondegenerate unit exists (2 ≥ 1), it changes the coherence quantum
observably, and at the rung table the coefficient-4 deformation meets every
banked clause while changing predictions. Minimality is the only selection
principle on the table, and it is a principle, not a theorem. -/
theorem dofPricing_boundary_without_minimality (Z : ℤ) :
    (1 ≤ (2 : ℤ))
    ∧ phi ^ ((2 : ℤ) * 5) ≠ phi ^ ((1 : ℤ) * 5)
    ∧ (∀ f : Fermion,
        shiftedRungs 2 f
          = (2 + 2) * activeChannelClasses f + Integers.tau (genOf f).val
            + (if f = Fermion.nu3 then 2 else 0))
    ∧ predictAt .Lepton (deformedTotal 2 Fermion.e) Z
        ≠ predictAt .Lepton (deformedTotal 0 Fermion.e) Z :=
  ⟨by norm_num, ecoh_differs_without_minimality,
    channel_cost_independent_without_premises Z⟩

What this page does not claim

The minimality principle is not proved, only assumed as a modeling choice. The theorem does not derive the value of any specific particle mass, only the base coefficient of the pricing rule. The result does not apply to pricing rules that allow fractional rung units per degree of freedom.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Masses/DofPricing.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: