Encyclopedia Masses Masses Mass Genesis T10 Scale Bearing Deposit Parent Deposit Unit Ratio Select I

ARTICLE 3 claims 3 theorems

Masses Mass Genesis T10 Scale Bearing Deposit Parent Deposit Unit Ratio Select I

A single theorem ties a particle's deposit location to a vanishing cost, and then shows why that rule cannot be the whole story.

Verify this page

The zero-cost selection rule

The declaration deposit_unit_ratio_select_is_jcost_zero is a formal theorem in the Recognition Science framework's machine-checked library of formal theorems. It states a precise equivalence: a deposit location is selected by unit ratio exactly when the recognition cost of that location's absolute pre-weight is zero. In plainer terms, the framework models a ledger, a discrete record of events, where each possible deposit site carries a cost. The theorem proves that the condition "this site has the unit ratio" and the condition "this site costs nothing" are the same condition.

The proof is short and direct. The framework's cost function, Jcost, has a proved property: it equals zero only at the input value 1. The theorem's forward direction substitutes the unit ratio into that property. The reverse direction uses the same property to recover the unit ratio from the zero cost. Both directions rely on the fact that the pre-weight is always positive, which the library also proves. So the equivalence is not an assumption; it is a derived consequence of the cost function's defining behavior.

What the theorem does not claim is just as important. It does not say that this zero-cost rule actually selects a deposit location in the full theory. The library's own wall theorem, scale_bearing_deposit_parent_wall, shows that at the tier of cascade weights plus Jcost, no recognition-native organ forces a viable nonempty deposit location. The unit-ratio selection is called an "R4 costume" in the source: a surface-level rule that does not reach down to choose among rungs. The missing organ, the source says, lies outside cascade absolute weights and Jcost, perhaps in an emission absolute outside Q(phi) or a pattern-to-ratio map from ledger dynamics.

In Recognition Science, this distinction matters. The framework proves many structural facts, but it is explicit about which facts are theorems and which are open targets. Here the theorem is real, the selection rule is real, and the wall that blocks it is also real. The reader can see exactly what is established and exactly what remains open.

THEOREM deposit_unit_ratio_select_is_jcost_zero · IndisputableMonolith/Masses/MassGenesis/T10ScaleBearingDepositParent.lean
deposit_unit_ratio_select_is_jcost_zero · IndisputableMonolith/Masses/MassGenesis/T10ScaleBearingDepositParent.lean:114 
/-- **R4 costume.** Unit-ratio selection is J-cost vanishing on the absolute
pre-weight (`N-route-t10-genesis-predicate-selection-is-r4`). -/
theorem deposit_unit_ratio_select_is_jcost_zero {N : Nat} {a : Real} (ha : a ≠ 0)
    (k : Fin N) :
    DepositUnitRatioSelect a k ↔
      Cost.Jcost (omegaPreN a (k, commit)) = 0 := by
  have hpos : 0 < omegaPreN a (k, commit) := omegaPreN_pos ha _
  constructor
  · intro h; rw [h, Cost.Jcost_unit0]
  · intro h; exact (Cost.Jcost_eq_zero_iff _ hpos).mp h
THEOREM deposit_unit_ratio_select_is_jcost_zero · IndisputableMonolith/Masses/MassGenesis/T10ScaleBearingDepositParent.lean
deposit_unit_ratio_select_is_jcost_zero · IndisputableMonolith/Masses/MassGenesis/T10ScaleBearingDepositParent.lean:114 
/-- **R4 costume.** Unit-ratio selection is J-cost vanishing on the absolute
pre-weight (`N-route-t10-genesis-predicate-selection-is-r4`). -/
theorem deposit_unit_ratio_select_is_jcost_zero {N : Nat} {a : Real} (ha : a ≠ 0)
    (k : Fin N) :
    DepositUnitRatioSelect a k ↔
      Cost.Jcost (omegaPreN a (k, commit)) = 0 := by
  have hpos : 0 < omegaPreN a (k, commit) := omegaPreN_pos ha _
  constructor
  · intro h; rw [h, Cost.Jcost_unit0]
  · intro h; exact (Cost.Jcost_eq_zero_iff _ hpos).mp h
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 the zero-cost rule actually selects a deposit location in the full theory. The theorem does not claim that the unit ratio is a derived coupling or a fundamental constant. The theorem does not claim that the missing organ has been found.

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