Encyclopedia Gravity Gravity Seven Gaps Recognition Ratio Substrate Blocker No Bare Ledger Selector R

ARTICLE 4 claims 4 theorems

Gravity Seven Gaps Recognition Ratio Substrate Blocker No Bare Ledger Selector R

A machine-checked proof shows that a recognition ledger alone cannot reveal the sign of the force that shaped it, so the missing information must be added as new physical data.

Verify this page

The bare-ledger blocker

A recognition ledger is a discrete record of events and their costs. The question at hand is whether such a record, on its own, can tell you the sign of an underlying source: whether it is pulling or pushing. The declaration no_bare_ledger_selector_recovers_signed_source proves that it cannot. No function of a bare two-cell recognition ledger can universally recover the signed source of the exact unit-coupled witness family. The proof works by exhibiting two ledgers, one with source strength 1 and one with source strength -1, that are identical as bare ledgers. Since the required outputs differ, any proposed selector must fail on at least one of them.

This is not a statement about a particular method being too weak. It is a theorem, checked by a machine, that the information is simply not present. The bare ledger records costs, and the costs are blind to the sign of the source. Reversing the source orientation leaves every J-cost, and hence the entire bare recognition ledger, unchanged. Therefore, the signed deficit-source orientation is extra constitutive data, not information contained in the ledger. The theorem is a precise blocker: it identifies exactly what is missing before a certain ratio relation can be derived.

In Recognition Science, the framework proves that this missing premise is a signed deficit-source constitutive coupling. This is a model choice that supplies a source strength, defined as a coupling constant times a geometric deficit, coupled linearly to the total strain in the J-cost action. Once this named premise is supplied, J-stationarity derives the recognition-ratio bridge, and a nontrivial source-backed family exists. The blocker does not say the ratio relation is false; it says the bare ledger alone cannot force it. The positive result does not define the desired bridge as an assumption, because the missing premise mentions neither the ratio nor its logarithm.

The practical consequence is a rule for building theories: if you want a recognition ledger to imply a specific signed source, you must put that source into the model explicitly. The ledger will not invent it for you. This is a clean separation of what is derived from what is assumed, and it is the kind of result that keeps the framework honest about its own foundations.

THEOREM no_bare_ledger_selector_recovers_signed_source · IndisputableMonolith/Gravity/SevenGaps/RecognitionRatioSubstrateBlocker.lean
no_bare_ledger_selector_recovers_signed_source · IndisputableMonolith/Gravity/SevenGaps/RecognitionRatioSubstrateBlocker.lean:175 
/-- **THEOREM (the exact bare-ledger blocker).** No function of a bare
`RecognitionLedger (Fin 2)` can universally recover the signed source of
the exact unit-coupled witness family.  The ledgers at sources `1` and `-1`
are equal, while the required outputs are different.  Therefore signed
deficit-source orientation is extra constitutive data, not information
contained in the bare ledger. -/
theorem no_bare_ledger_selector_recovers_signed_source :
    ¬ ∃ select : RecognitionLedger.RecognitionLedger (Fin 2) → ℝ,
      RecoversSignedSourceFromBareLedger select := by
  rintro ⟨select, hselect⟩
  have hneg := hselect (-1)
  have hpos := hselect 1
  rw [signBlindBareLedger_neg_eq 1] at hneg
  norm_num at hneg hpos
  linarith
THEOREM signBlindBareLedger_neg_eq · IndisputableMonolith/Gravity/SevenGaps/RecognitionRatioSubstrateBlocker.lean
signBlindBareLedger_neg_eq · IndisputableMonolith/Gravity/SevenGaps/RecognitionRatioSubstrateBlocker.lean:142 
/-- **THEOREM (same bare ledger, opposite signed source).** Reversing the
source orientation leaves every J-cost, hence the entire bare recognition
ledger, unchanged. -/
theorem signBlindBareLedger_neg_eq (d : ℝ) :
    signBlindBareLedger (-d) = signBlindBareLedger d := by
  apply recognitionLedger_cost_ext
  funext i j
  rw [show (signBlindBareLedger (-d)).cost i j
      = Cost.Jcost ((twoHingeWitnessBridge (-d)).xRatio i
          / (twoHingeWitnessBridge (-d)).xRatio j) from
        ratioBridgeLedger_cost (twoHingeWitnessBridge (-d)) i j]
  rw [show (signBlindBareLedger d).cost i j
      = Cost.Jcost ((twoHingeWitnessBridge d).xRatio i
          / (twoHingeWitnessBridge d).xRatio j) from
        ratioBridgeLedger_cost (twoHingeWitnessBridge d) i j]
  have hratio :
      (twoHingeWitnessBridge (-d)).xRatio i
          / (twoHingeWitnessBridge (-d)).xRatio j
        = ((twoHingeWitnessBridge d).xRatio i
            / (twoHingeWitnessBridge d).xRatio j)⁻¹ := by
    rw [twoHingeWitnessBridge_xRatio_neg d i,
      twoHingeWitnessBridge_xRatio_neg d j, inv_div_inv, inv_div]
  rw [hratio]
  exact (Cost.Jcost_symm
    (div_pos ((twoHingeWitnessBridge d).xRatio_pos i)
      ((twoHingeWitnessBridge d).xRatio_pos j))).symm
THEOREM no_bare_ledger_selector_recovers_signed_source · IndisputableMonolith/Gravity/SevenGaps/RecognitionRatioSubstrateBlocker.lean
no_bare_ledger_selector_recovers_signed_source · IndisputableMonolith/Gravity/SevenGaps/RecognitionRatioSubstrateBlocker.lean:175 
/-- **THEOREM (the exact bare-ledger blocker).** No function of a bare
`RecognitionLedger (Fin 2)` can universally recover the signed source of
the exact unit-coupled witness family.  The ledgers at sources `1` and `-1`
are equal, while the required outputs are different.  Therefore signed
deficit-source orientation is extra constitutive data, not information
contained in the bare ledger. -/
theorem no_bare_ledger_selector_recovers_signed_source :
    ¬ ∃ select : RecognitionLedger.RecognitionLedger (Fin 2) → ℝ,
      RecoversSignedSourceFromBareLedger select := by
  rintro ⟨select, hselect⟩
  have hneg := hselect (-1)
  have hpos := hselect 1
  rw [signBlindBareLedger_neg_eq 1] at hneg
  norm_num at hneg hpos
  linarith
THEOREM recognition_ratio_derived_of_deficit_source_coupling · nontrivial_source_backed_family_exists · IndisputableMonolith/Gravity/SevenGaps/RecognitionRatioSubstrateBlocker.lean
recognition_ratio_derived_of_deficit_source_coupling · IndisputableMonolith/Gravity/SevenGaps/RecognitionRatioSubstrateBlocker.lean:97 
/-- **THEOREM (the conditional `recognition_ratio_derived`).** Once the
named deficit-source constitutive coupling is supplied, J-stationarity
derives the bridge relation with explicit remainder constant `n / 6`.
No hypothesis states a fact about `xRatio` or `log xRatio`. -/
theorem recognition_ratio_derived_of_deficit_source_coupling {H : Type*}
    (C : DeficitSourceConstitutiveCoupling H) (σ : H) :
    |Real.log ((ratioBridgeFromDeficitSourceCoupling C).xRatio σ)
        - C.kappa σ * C.geometricDeficit σ|
      ≤ (C.channels : ℝ) / 6 * C.meshScale ^ 3 :=
  (ratioBridgeFromDeficitSourceCoupling C).ratio_relation σ
nontrivial_source_backed_family_exists · IndisputableMonolith/Gravity/SevenGaps/RecognitionRatioSubstrateBlocker.lean:193 
/-- **THEOREM (nontrivial source-backed family).** For every nonzero
coupling and positive channel count, the quadratic sourced family is
uniformly admissible.  Its source is exactly `n*h^2`, and at every nonzero
mesh both its geometric deficit and stationary log-ratio are nonzero.
Thus the conditional positive route is populated by a genuine small-mesh
family rather than a zero-source or fixed-mesh witness. -/
theorem nontrivial_source_backed_family_exists
    (n : ℕ) (hn : 1 ≤ n) (h₀ kappa : ℝ) (hκ : kappa ≠ 0) :
    ∃ F : RecognitionRatioFamily,
      F.IsAdmissible h₀ kappa ((n : ℝ) / |kappa|)
          ((n : ℝ) * h₀ ^ 3 / 6) ∧
      (∀ h, kappa * F.deficit h = (n : ℝ) * h ^ 2) ∧
      (∀ h, h ≠ 0 →
        F.deficit h ≠ 0 ∧ 0 < Real.log (F.ratio h)) := by
  refine ⟨quadraticSourceFamily n kappa,
    quadraticSourceFamily_isAdmissible n hn h₀ kappa hκ, ?_, ?_⟩
  · intro h
    show kappa * ((n : ℝ) / kappa * h ^ 2) = (n : ℝ) * h ^ 2
    field_simp
  · intro h hh
    exact ⟨quadraticSourceFamily_deficit_ne_zero n hn kappa h hκ hh,
      quadraticSourceFamily_logRatio_pos n hn kappa h hκ hh⟩

What this page does not claim

This does not claim that the recognition ratio is false or unattainable, only that it is not a consequence of the bare ledger alone. This does not claim that a specific physical source exists, only that a formal model with that structure is admissible. This does not claim that the signed source can never be inferred from other data, only that it cannot be inferred from the bare two-cell ledger.

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/Gravity/SevenGaps/RecognitionRatioSubstrateBlocker.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