Foundation Measurement Mechanism Lower Defect Higher Weight

The weighting rule

In the Recognition Science framework, a ledger (a discrete record of events) assigns each possible configuration a numerical weight. The theorem named lower_defect_higher_weight states that if configuration A has a strictly smaller total defect than configuration B, then A's weight is strictly greater than B's. The weight is defined as the exponential of the negative total defect: jcost_weight(c) = exp(-total_defect(c)). Because the exponential function is strictly increasing, a smaller defect means a less negative exponent, which means a larger weight.

This is a formal statement in the framework's machine-checked library of formal theorems. It is a direct consequence of the definition of weight and the monotonicity of the exponential function. The theorem does not specify what a defect is, how it is calculated, or why this particular weighting is chosen. Those are separate definitions and modeling choices. The theorem only establishes the ordering: lower defect implies higher weight.

In Recognition Science, this weighting rule is a component of a proposed measurement mechanism. The framework models an observer as a subsystem of the ledger, with access only to its own entries. The full configuration determines the outcome of a measurement, but the observer's partial view does not. The weighting rule is used to connect the cost of a configuration to its statistical weight, a step toward a Born-rule-like structure. The theorem itself, however, does not make any claim about quantum mechanics or the Born rule; it is a statement about the ordering of weights.

/-- Lower defect ↔ higher weight. The cost landscape determines the
    probability landscape. -/
theorem lower_defect_higher_weight {N : ℕ}
    (c₁ c₂ : Configuration N)
    (h : total_defect c₁ < total_defect c₂) :
    jcost_weight c₂ < jcost_weight c₁ := by
  unfold jcost_weight
  exact Real.exp_lt_exp_of_lt (neg_lt_neg h)

/-- The **J-cost weight** of a configuration: exp(-total_defect).
    Configurations with lower defect have higher weight.
    This is the analogue of the Boltzmann weight in statistical mechanics
    and the |ψ|² weight in quantum mechanics. -/
noncomputable def jcost_weight {N : ℕ} (c : Configuration N) : ℝ :=
  Real.exp (-total_defect c)

What this page does not claim

The theorem does not define what a defect is or how it is calculated. The theorem does not by itself establish the Born rule or any quantum mechanical result. The theorem does not claim that this weighting is empirically correct.

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