Encyclopedia Masses Masses Mass Genesis T10 Scale Bearing Deposit Parent Cascade Weight Ratio Count

ARTICLE 3 claims 3 theorems

Masses Mass Genesis T10 Scale Bearing Deposit Parent Cascade Weight Ratio Count

A theorem about mass-formation weights strips away a scale factor and leaves a ratio that depends only on counting, not on overall size.

Verify this page

What the ratio theorem shows

In the Recognition Science account of how particle masses form, each candidate location in a discrete structure carries a numerical weight called a cascade weight. The theorem cascade_weight_ratio_count_visible states a clean fact about ratios of these weights: when you divide one location's cascade weight by another's, the common scale factor cancels out. The ratio equals a quotient of two simple expressions, each built from the golden ratio raised to a position index plus a count of deposits at that position. The result is that the ratio is completely blind to the overall amplitude of the process; it sees only the relative positions and the deposit counts.

This is a theorem in the machine-checked library, meaning it is proved from definitions by symbolic algebra, not assumed. The proof is a direct calculation: the cascade weight factors into a common posting-event load times a position-and-count term, and that common factor cancels in the ratio. The statement holds for any nonzero scale parameter and any finite list of deposit locations, so it is fully general within the model. What it establishes is a precise sense in which ratios of cascade weights are count-visible: they reveal the counting data, not the overall scale.

What the theorem does not claim is that these ratios select where deposits actually occur. A separate wall theorem in the same framework shows that, at the tier of absolute cascade weights plus recognition cost, no recognition-native mechanism forces a viable nonempty deposit location without collapsing to a killed shape. The ratio theorem is a component of that wall, not a location selector. It also does not say that deposit counts alone determine the full weight, only the ratios. And it does not imply that the golden ratio itself is derived here; the golden ratio enters as a predefined scale in the model.

THEOREM cascade_weight_ratio_count_visible · IndisputableMonolith/Masses/MassGenesis/T10ScaleBearingDepositParent.lean
cascade_weight_ratio_count_visible · IndisputableMonolith/Masses/MassGenesis/T10ScaleBearingDepositParent.lean:57 
theorem cascade_weight_ratio_count_visible {N : Nat} {a : Real} (ha : a ≠ 0)
    (ks : List (Fin N)) (i j : SectorN N) :
    omegaCascade a ks i / omegaCascade a ks j =
      (phi ^ i.1.val + (depositCount ks i.1 : Real)) /
        (phi ^ j.1.val + (depositCount ks j.1 : Real)) := by
  obtain ⟨n, p⟩ := i
  obtain ⟨m, q⟩ := j
  have hload : postingEventLoad a ≠ 0 := ne_of_gt (postingEventLoad_pos ha)
  rw [omegaCascade_factor_amplitude, omegaCascade_factor_amplitude]
  field_simp [hload]
THEOREM cascade_weight_ratio_count_visible · IndisputableMonolith/Masses/MassGenesis/T10ScaleBearingDepositParent.lean
cascade_weight_ratio_count_visible · IndisputableMonolith/Masses/MassGenesis/T10ScaleBearingDepositParent.lean:57 
theorem cascade_weight_ratio_count_visible {N : Nat} {a : Real} (ha : a ≠ 0)
    (ks : List (Fin N)) (i j : SectorN N) :
    omegaCascade a ks i / omegaCascade a ks j =
      (phi ^ i.1.val + (depositCount ks i.1 : Real)) /
        (phi ^ j.1.val + (depositCount ks j.1 : Real)) := by
  obtain ⟨n, p⟩ := i
  obtain ⟨m, q⟩ := j
  have hload : postingEventLoad a ≠ 0 := ne_of_gt (postingEventLoad_pos ha)
  rw [omegaCascade_factor_amplitude, omegaCascade_factor_amplitude]
  field_simp [hload]
THEOREM scale_bearing_deposit_parent_wall · IndisputableMonolith/Masses/MassGenesis/T10ScaleBearingDepositParent.lean
scale_bearing_deposit_parent_wall · IndisputableMonolith/Masses/MassGenesis/T10ScaleBearingDepositParent.lean:137 
/-- **SCALE-BEARING DEPOSIT-PARENT WALL (THEOREM), cascade-weight + J-cost tier.**

At the named tier of principles whose observable data is a function of
absolute cascade weights together with recognition cost `Jcost`:

* ratios of cascade weights are count-visible and amplitude-blind (C4 tier);
* total posted-load recognition ratios are length-only (location-blind);
* unit-ratio / J-cost-vanishing selection is R4 costume;
* continuum field-escape remains uniform on the C4 closed set (Attack 1
  disposition: completing the even residual cannot restore selection).

No recognition-native organ at this tier forces a viable nonempty deposit
location without collapsing to a killed shape. The missing organ lies outside
cascade absolute weights and `Jcost` (an emission absolute outside `Q(phi)`,
or a pattern-to-ratio map from ledger dynamics). -/
theorem scale_bearing_deposit_parent_wall {N : Nat} (hN : 2 ≤ N) {a : Real}
    (ha : a ≠ 0) :
    (∀ (ks : List (Fin N)) (i j : SectorN N),
      omegaCascade a ks i / omegaCascade a ks j =
        (phi ^ i.1.val + (depositCount ks i.1 : Real)) /
          (phi ^ j.1.val + (depositCount ks j.1 : Real))) ∧
    (∀ (ks ks' : List (Fin N)), ks.length = ks'.length →
      postedLoad a ks / postedLoad a ([] : List (Fin N)) =
        postedLoad a ks' / postedLoad a ([] : List (Fin N))) ∧
    (∀ (k : Fin N),
      DepositUnitRatioSelect a k ↔
        Cost.Jcost (omegaPreN a (k, commit)) = 0) ∧
    (∀ (k1 k2 : Nat),
      (Odd k1 ∨ k1 = 0 ∨ k1 = 1) →
        (Odd k2 ∨ k2 = 0 ∨ k2 = 1) →
          (¬ InQPhi (Real.sqrt ((1 + phi ^ k1) / phi ^ k1))) ∧
            (¬ InQPhi (Real.sqrt ((1 + phi ^ k2) / phi ^ k2)))) ∧
    (∀ (ks ks' : List (Fin N)),
      (∀ n, depositCount ks n = depositCount ks' n) →
        cascadeSpectrum ks = cascadeSpectrum ks') := by
  refine ⟨?_, ?_, ?_, ?_, ?_⟩
  · intro ks i j; exact cascade_weight_ratio_count_visible ha ks i j
  · intro ks ks' hlen
    exact postedLoad_ratio_length_only ha (by omega) ks ks' hlen
  · intro k; exact deposit_unit_ratio_select_is_jcost_zero ha k
  · intro k1 k2 h1 h2; exact even_sqrt_escape_does_not_select_by_uniformity h1 h2
  · intro ks ks' hc; exact cascade_order_blind ha ks ks' hc

What this page does not claim

The theorem does not claim that ratios select where deposits occur. It does not claim that deposit counts alone determine the full weight, only the ratios. It does not claim that the golden ratio is derived here; it enters as a predefined scale.

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/T10ScaleBearingDepositParent.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:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND