Masses Mass Genesis Factorized Load Density Charge Gap Load Exponent Unfold

The charge gap exponent

The charge gap exponent is a real number attached to a light pattern, a discrete configuration of events in the framework's ledger, a record of recognition events. The declaration chargeGapLoadExponent_unfold establishes that this exponent is computed by a specific formula: the base-phi logarithm of one plus the pattern's charge gap Z divided by phi. In plainer terms, the exponent measures how much the charge gap, a quantity derived from the pattern's topology, shifts the power of phi that scales the mass. The statement is proved by unfolding the definition; it is a direct identity, not a derivation from deeper principles.

The context matters. The framework's mass law predicts a particle's mass as a power of phi, the golden ratio, and the charge gap exponent is one of three factors that multiply together to give that mass. The other two are a sector geometry factor and a rung exponent. The declaration shows that the charge gap exponent is exactly the logarithm of the gap, which is a concrete, checkable statement. It does not show that stable light dynamics forces this exponent; that remains an open target. The next step must derive a site load density summing to the exact factorized expression.

What the declaration does not claim is as important as what it proves. It does not claim that the charge gap exponent is derived from the framework's forcing chain, the sequence of statements that fixes constants and dimensions. It does not claim that the mass law itself is proved; the mass law is a definitional target, and the factorized expression is a reformulation of that target, not a proof of it. The declaration only unpacks a definition, showing what the exponent is in terms of the charge gap. It leaves the physical bridge, the step from stable light dynamics to the density, open.

theorem chargeGapLoadExponent_unfold (ψ : LightPattern Λ) :
    chargeGapLoadExponent ψ =
      Real.log (1 + (ZOf ψ : ℝ) / Constants.phi) /
        Real.log Constants.phi := rfl

/-- The factorized MassLaw load target, written as sector geometry times one
phi exponent assembled from rung and charge-gap pieces. -/
noncomputable def factorizedMassLawLoad (ψ : LightPattern Λ) : ℝ :=
  sectorLoadFactor ψ *
    Constants.phi ^ (rungLoadExponent ψ + chargeGapLoadExponent ψ)

What this page does not claim

The charge gap exponent is not derived from the framework's forcing chain. The mass law itself is not proved by this declaration. No claim is made that the factorized expression is unique.

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/MassGenesis/FactorizedLoadDensity.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: