Encyclopedia Foundation Foundation Measure Forcing Cont Weight Satisfies Premises
ARTICLE 4 claims 4 theorems
Foundation Measure Forcing Cont Weight Satisfies Premises
A single rule for how much reality sits in each recognition state follows from two plain premises, and it is the golden ratio again.
The forced weighting
A recognition event is a discrete record of a distinction being made. The Recognition Science framework asks: given the allowed recognition states, how much of reality sits in each one? The declaration contWeight_satisfies_premises establishes that any admissible weighting of continuous recognition states must be the geometric measure: weight φ−t for a state at cost t, where φ is the golden ratio. Equivalently, the probability of a state is proportional to exp(−(ln φ)·t), a Gibbs rule with the rate pinned by the self-similar ledger, not chosen.
The result rests on two premises. First, factorization over independent composition: the weight of a composite of independent recognition steps is the product of the weights. This is the multiplicative shadow of ledger cost additivity. Second, per-step self-similar balance: the single-step weight satisfies ρ = 1/(1+ρ), the reciprocal self-similarity fixed point. Conditional on that equation, the framework forces ρ = φ−1. The theorem continuum_weight_forced proves that for all t ≥ 0, f(t) = ρt, not merely within a power-law class: the multiplicative Cauchy equation plus monotonicity pins the function on the rationals by roots and on the irrationals by an elementary squeeze.
The forced measure has structure constants. The partition function Z = Σ φ−n = φ², the ground-state share P(0) = φ−2, and the mean occupied rung ⟨n⟩ = φ exactly. Five previously separate dilution and occupancy laws in the library are one object: the forced measure. The identifications include θ = φ−4 = w(4), ℏ = φ−5 = w(5), and rung-44 scale φ−44 = w(44).
In Recognition Science, the measure is cost-sufficient: equal-cost mirror states get equal weight. So chirality selection cannot come from the forced measure at equal J; it requires a J-asymmetry or spontaneous breaking. The full Born bridge to recognition Hilbert space remains open, as does the H-theorem: the framework forces the unique stationary weighting, but convergence to it is not yet proved.
THEOREM continuum_weight_forced · IndisputableMonolith/Foundation/MeasureForcing.lean
/-- **T9, CONTINUUM LAYER (full uniqueness).** Any factorizing, antitone
weight with the calibrated step `f(1) = φ⁻¹` equals `φ⁻ᵗ` at every
`t ≥ 0`. No power-law-class restriction: this is the multiplicative
Cauchy equation pinned by monotonicity. -/
theorem continuum_weight_forced (hadd : Factorizes f)
(hanti : AntitoneOn f (Set.Ici 0)) (hstep : f 1 = rho) :
∀ t : ℝ, 0 ≤ t → f t = rho ^ t := by
intro t ht
rcases eq_or_lt_of_le ht with h0 | hpos
· rw [← h0, Real.rpow_zero]
exact f_zero hadd hanti hstep
-- t > 0. Set L := f t and squeeze with rationals.
set L : ℝ := f t with hL
-- upper rationals: t ≤ q ⇒ ρ^q ≤ L
have hub : ∀ q : ℚ, t ≤ (q : ℝ) → rho ^ ((q : ℝ)) ≤ L := by
intro q hq
have hq0 : (0 : ℝ) ≤ (q : ℝ) := le_trans hpos.le hq
have := hanti (Set.mem_Ici.mpr hpos.le) (Set.mem_Ici.mpr hq0) hq
rwa [f_ratCast hadd hanti hstep q hq0] at this
-- lower rationals: 0 ≤ q ≤ t ⇒ L ≤ ρ^q
have hlb : ∀ q : ℚ, 0 ≤ (q : ℝ) → (q : ℝ) ≤ t → L ≤ rho ^ ((q : ℝ)) := by
intro q hq0 hq
have := hanti (Set.mem_Ici.mpr hq0) (Set.mem_Ici.mpr hpos.le) hq
rwa [f_ratCast hadd hanti hstep q hq0] at this
-- L > 0
have hLpos : 0 < L := by
obtain ⟨q, hq⟩ := exists_rat_gt t
exact lt_of_lt_of_le (Real.rpow_pos_of_pos rho_pos _) (hub q hq.le)
have hrt_pos : 0 < rho ^ t := Real.rpow_pos_of_pos rho_pos t
have hlogrho_neg : Real.log rho < 0 := Real.log_neg rho_pos rho_lt_one
-- trichotomy
rcases lt_trichotomy L (rho ^ t) with hlt | heq | hgt
· -- L < ρ^t: find rational q > t with ρ^q > L. Contradiction with hub.
exfalso
have hlog : Real.log L < t * Real.log rho := by
have := Real.log_lt_log hLpos hlt
rwa [Real.log_rpow rho_pos] at this
have hkey : t < Real.log L / Real.log rho := by
rw [lt_div_iff_of_neg hlogrho_neg]
linarith [hlog]
obtain ⟨q, hq1, hq2⟩ := exists_rat_btwn hkey
have hcontra : L < rho ^ ((q : ℝ)) := by
have hq2' : Real.log L < (q : ℝ) * Real.log rho := by
have := (lt_div_iff_of_neg hlogrho_neg).mp hq2
linarith
have : Real.exp (Real.log L) < Real.exp (Real.log rho * (q : ℝ)) := by
rw [Real.exp_lt_exp]; linarith
rwa [Real.exp_log hLpos, ← Real.rpow_def_of_pos rho_pos] at this
exact absurd (hub q hq1.le) (not_le.mpr hcontra)
· exact heq
· -- L > ρ^t: find rational 0 ≤ q < t with ρ^q < L. Contradiction with hlb.
exfalso
have hlog : t * Real.log rho < Real.log L := by
have := Real.log_lt_log hrt_pos hgt
rwa [Real.log_rpow rho_pos] at this
have hkey : Real.log L / Real.log rho < t := by
rw [div_lt_iff_of_neg hlogrho_neg]
linarith [hlog]
have hmax : max (Real.log L / Real.log rho) 0 < t := max_lt hkey hpos
obtain ⟨q, hq1, hq2⟩ := exists_rat_btwn hmax
have hq0 : (0 : ℝ) ≤ (q : ℝ) :=
le_of_lt (lt_of_le_of_lt (le_max_right _ _) hq1)
have hcontra : rho ^ ((q : ℝ)) < L := by
have hqgt : Real.log L / Real.log rho < (q : ℝ) :=
lt_of_le_of_lt (le_max_left _ _) hq1
have hq2' : (q : ℝ) * Real.log rho < Real.log L := by
have := (div_lt_iff_of_neg hlogrho_neg).mp hqgt
linarith
have : Real.exp (Real.log rho * (q : ℝ)) < Real.exp (Real.log L) := by
rw [Real.exp_lt_exp]; linarith
rwa [Real.exp_log hLpos, ← Real.rpow_def_of_pos rho_pos] at this
exact absurd (hlb q hq0 hq2.le) (not_le.mpr hcontra)
THEOREM probMass · IndisputableMonolith/Foundation/MeasureForcing.lean
/-- The normalized probability mass at `n` steps: `P(n) = (1−ρ)·ρⁿ`. -/
def probMass (n : ℕ) : ℝ := (1 - rho) * rho ^ n
THEOREM meanRung_eq_phi · IndisputableMonolith/Foundation/MeasureForcing.lean
/-- **`⟨n⟩ = φ` exactly.** The mean recognition depth of the forced
measure is the golden ratio itself. -/
theorem meanRung_eq_phi : meanRung = Constants.phi := by
unfold meanRung
have hre : (fun n : ℕ => (n : ℝ) * probMass n)
= fun n : ℕ => (1 - rho) * ((n : ℝ) * rho ^ n) := by
funext n; unfold probMass; ring
rw [hre, tsum_mul_left]
have hnorm : ‖rho‖ < 1 := by
rw [Real.norm_eq_abs, abs_of_pos rho_pos]; exact rho_lt_one
rw [tsum_coe_mul_geometric_of_norm_lt_one hnorm]
-- (1 − ρ) · ρ/(1−ρ)² = ρ/(1−ρ) = φ⁻¹·φ² = φ
rw [one_sub_rho]
unfold rho
have hphi : Constants.phi ≠ 0 := phi_ne_zero
field_simp
THEOREM weight_blind_to_label · IndisputableMonolith/Foundation/MeasureForcing.lean
/-- **CHIRALITY NO-GO.** Any cost-sufficient weight assigns equal weight
to the two mirror labels at every cost. -/
theorem weight_blind_to_label (W : CostSufficientWeight) (c : ℝ) :
W.w ⟨c, true⟩ = W.w ⟨c, false⟩ :=
W.cost_sufficient _ _ rfl
What this page does not claim
The per-step self-similar balance premise is not proved; it is a hypothesis with a named falsifier. The Born rule bridge to recognition Hilbert space is not established. The H-theorem, convergence to the forced measure, is not proved.
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/Foundation/MeasureForcing.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:
- What physical principle selects the per-step self-similar balance premise?
- Does the forced measure converge to equilibrium from arbitrary initial weightings?
- What is the recognition Hilbert space in which the Born rule would hold?
MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND
THEOREM continuum_weight_forced · IndisputableMonolith/Foundation/MeasureForcing.lean
/-- **T9, CONTINUUM LAYER (full uniqueness).** Any factorizing, antitone weight with the calibrated step `f(1) = φ⁻¹` equals `φ⁻ᵗ` at every `t ≥ 0`. No power-law-class restriction: this is the multiplicative Cauchy equation pinned by monotonicity. -/ theorem continuum_weight_forced (hadd : Factorizes f) (hanti : AntitoneOn f (Set.Ici 0)) (hstep : f 1 = rho) : ∀ t : ℝ, 0 ≤ t → f t = rho ^ t := by intro t ht rcases eq_or_lt_of_le ht with h0 | hpos · rw [← h0, Real.rpow_zero] exact f_zero hadd hanti hstep -- t > 0. Set L := f t and squeeze with rationals. set L : ℝ := f t with hL -- upper rationals: t ≤ q ⇒ ρ^q ≤ L have hub : ∀ q : ℚ, t ≤ (q : ℝ) → rho ^ ((q : ℝ)) ≤ L := by intro q hq have hq0 : (0 : ℝ) ≤ (q : ℝ) := le_trans hpos.le hq have := hanti (Set.mem_Ici.mpr hpos.le) (Set.mem_Ici.mpr hq0) hq rwa [f_ratCast hadd hanti hstep q hq0] at this -- lower rationals: 0 ≤ q ≤ t ⇒ L ≤ ρ^q have hlb : ∀ q : ℚ, 0 ≤ (q : ℝ) → (q : ℝ) ≤ t → L ≤ rho ^ ((q : ℝ)) := by intro q hq0 hq have := hanti (Set.mem_Ici.mpr hq0) (Set.mem_Ici.mpr hpos.le) hq rwa [f_ratCast hadd hanti hstep q hq0] at this -- L > 0 have hLpos : 0 < L := by obtain ⟨q, hq⟩ := exists_rat_gt t exact lt_of_lt_of_le (Real.rpow_pos_of_pos rho_pos _) (hub q hq.le) have hrt_pos : 0 < rho ^ t := Real.rpow_pos_of_pos rho_pos t have hlogrho_neg : Real.log rho < 0 := Real.log_neg rho_pos rho_lt_one -- trichotomy rcases lt_trichotomy L (rho ^ t) with hlt | heq | hgt · -- L < ρ^t: find rational q > t with ρ^q > L. Contradiction with hub. exfalso have hlog : Real.log L < t * Real.log rho := by have := Real.log_lt_log hLpos hlt rwa [Real.log_rpow rho_pos] at this have hkey : t < Real.log L / Real.log rho := by rw [lt_div_iff_of_neg hlogrho_neg] linarith [hlog] obtain ⟨q, hq1, hq2⟩ := exists_rat_btwn hkey have hcontra : L < rho ^ ((q : ℝ)) := by have hq2' : Real.log L < (q : ℝ) * Real.log rho := by have := (lt_div_iff_of_neg hlogrho_neg).mp hq2 linarith have : Real.exp (Real.log L) < Real.exp (Real.log rho * (q : ℝ)) := by rw [Real.exp_lt_exp]; linarith rwa [Real.exp_log hLpos, ← Real.rpow_def_of_pos rho_pos] at this exact absurd (hub q hq1.le) (not_le.mpr hcontra) · exact heq · -- L > ρ^t: find rational 0 ≤ q < t with ρ^q < L. Contradiction with hlb. exfalso have hlog : t * Real.log rho < Real.log L := by have := Real.log_lt_log hrt_pos hgt rwa [Real.log_rpow rho_pos] at this have hkey : Real.log L / Real.log rho < t := by rw [div_lt_iff_of_neg hlogrho_neg] linarith [hlog] have hmax : max (Real.log L / Real.log rho) 0 < t := max_lt hkey hpos obtain ⟨q, hq1, hq2⟩ := exists_rat_btwn hmax have hq0 : (0 : ℝ) ≤ (q : ℝ) := le_of_lt (lt_of_le_of_lt (le_max_right _ _) hq1) have hcontra : rho ^ ((q : ℝ)) < L := by have hqgt : Real.log L / Real.log rho < (q : ℝ) := lt_of_le_of_lt (le_max_left _ _) hq1 have hq2' : (q : ℝ) * Real.log rho < Real.log L := by have := (div_lt_iff_of_neg hlogrho_neg).mp hqgt linarith have : Real.exp (Real.log rho * (q : ℝ)) < Real.exp (Real.log L) := by rw [Real.exp_lt_exp]; linarith rwa [Real.exp_log hLpos, ← Real.rpow_def_of_pos rho_pos] at this exact absurd (hlb q hq0 hq2.le) (not_le.mpr hcontra)The theorem continuum_weight_forced proves that for all t ≥ 0, f(t) = ρ<sup>t</sup>, not merely within a power-law class. continuum_weight_forced · IndisputableMonolith/Foundation/MeasureForcing.leanTHEOREM probMass · IndisputableMonolith/Foundation/MeasureForcing.lean
/-- The normalized probability mass at `n` steps: `P(n) = (1−ρ)·ρⁿ`. -/ def probMass (n : ℕ) : ℝ := (1 - rho) * rho ^ nThe partition function Z = Σ φ<sup>−n</sup> = φ². probMass · IndisputableMonolith/Foundation/MeasureForcing.leanTHEOREM meanRung_eq_phi · IndisputableMonolith/Foundation/MeasureForcing.lean
/-- **`⟨n⟩ = φ` exactly.** The mean recognition depth of the forced measure is the golden ratio itself. -/ theorem meanRung_eq_phi : meanRung = Constants.phi := by unfold meanRung have hre : (fun n : ℕ => (n : ℝ) * probMass n) = fun n : ℕ => (1 - rho) * ((n : ℝ) * rho ^ n) := by funext n; unfold probMass; ring rw [hre, tsum_mul_left] have hnorm : ‖rho‖ < 1 := by rw [Real.norm_eq_abs, abs_of_pos rho_pos]; exact rho_lt_one rw [tsum_coe_mul_geometric_of_norm_lt_one hnorm] -- (1 − ρ) · ρ/(1−ρ)² = ρ/(1−ρ) = φ⁻¹·φ² = φ rw [one_sub_rho] unfold rho have hphi : Constants.phi ≠ 0 := phi_ne_zero field_simpThe mean occupied rung ⟨n⟩ = φ exactly. meanRung_eq_phi · IndisputableMonolith/Foundation/MeasureForcing.leanTHEOREM weight_blind_to_label · IndisputableMonolith/Foundation/MeasureForcing.lean
/-- **CHIRALITY NO-GO.** Any cost-sufficient weight assigns equal weight to the two mirror labels at every cost. -/ theorem weight_blind_to_label (W : CostSufficientWeight) (c : ℝ) : W.w ⟨c, true⟩ = W.w ⟨c, false⟩ := W.cost_sufficient _ _ rflThe measure is cost-sufficient: equal-cost mirror states get equal weight. weight_blind_to_label · IndisputableMonolith/Foundation/MeasureForcing.lean