Pith. sign in
module module low

IndisputableMonolith.Physics.Superposition3_FromJCost

show as:
view Lean formalization →

Packages a three-domain superposition certificate built from the RS J-cost. Defines a domain cost functional, a positive canonical threshold, nonnegativity facts, and an inhabited Superpos3Cert record. Interference and multi-path arguments in Recognition Physics would cite it. The module is mostly definitional, with short positivity and evaluation lemmas.

claimFrom the RS cost $J$, define a domain cost on three labeled domains, a canonical threshold $\tau>0$, and a certificate asserting that the three domain costs jointly satisfy the superposition bound relative to $\tau$. The certificate type is inhabited.

background

Recognition Science measures mismatch with the unique cost $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$), forced at T5 of the unified chain. The Cost import supplies that functional and its elementary identities; Constants supplies the RS tick scale.

This module lifts $J$ to a per-domain cost on three channels (the natural count once $D=3$ spatial dimensions and the eight-tick octave are in place). A single positive threshold is fixed as the comparison scale against which the three domain costs are judged.

The local goal is not a full dynamical superposition law, but a static certificate: three domain costs and the threshold package into a record that later physics lemmas can assume or inhabit.

proof idea

Definition module with thin lemmas. domainCost evaluates the J-derived cost on a domain label; domainCost_at_eq is an evaluation identity; domainCost_nonneg records nonnegativity of $J$ on the positive reals. canonicalThreshold picks the comparison scale; canonicalThreshold_pos proves it is positive. Superpos3Cert is the certificate structure; cert and cert_inhabited supply a concrete inhabitant. No deep tactic proof: algebraic nonnegativity and a one-line inhabitation.

why it matters in Recognition Science

Gives Physics a named three-way superposition certificate tied directly to J-cost rather than an ad hoc norm. Downstream multi-path or interference developments can depend on Superpos3Cert instead of re-deriving domain nonnegativity. Aligns with the forcing landmarks T5 (J uniqueness), T7 (eight-tick octave), and T8 ($D=3$), which together make three spatial channels the default counting. No used_by edges are recorded yet; the module is a leaf provider for later physics certificates.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (8)