Pith. sign in
module module moderate

IndisputableMonolith.Foundation.WaveParticleDuality3FromJCost

show as:
view Lean formalization →

Packages a three-mode wave-particle duality certificate built from the RS J-cost. Defines a domain cost, a positive canonical threshold, and an inhabited certificate type WPDuality3Cert. Cited by foundation audits that need a Lean-side witness that particle, wave, and dual regimes sit on one J-derived cost scale. Structure is definitional plus elementary nonnegativity and positivity lemmas.

claimFrom the RS cost $J$, define a domain cost $C$ on positive reals, a canonical threshold $\theta>0$, and a certificate type asserting three-regime wave-particle duality: particle-like, wave-like, and dual regimes separated by $\theta$ on the $J$-scale, with $C\ge 0$ and $C$ agreeing with $J$ at the identity.

background

Recognition Science forces a unique symmetric cost $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$) via the Recognition Composition Law and the T5 uniqueness step. That cost is the yardstick for comparing recognition defects across scales.

This module sits in the Foundation layer and imports only Constants (RS time quantum $\tau_0=1$ tick) and Cost (the $J$ infrastructure). It specializes the cost to a domain-level functional used to separate three kinematic regimes rather than to derive masses or coupling constants.

The local objects are a domain cost, its value at equality, nonnegativity, a canonical positive threshold, and a certificate record WPDuality3Cert together with an inhabited instance. The "3" marks the three-regime split (particle / wave / dual), aligned with the broader RS claim that spatial dimension $D=3$ is forced (T8), not a free parameter.

proof idea

Definition module with thin lemmas, not a deep derivation. domainCost is introduced from $J$; domainCost_at_eq and domainCost_nonneg record the identity value and nonnegativity inherited from $J$. canonicalThreshold and canonicalThreshold_pos fix a positive cut on that cost scale. WPDuality3Cert is a structure bundling those facts; cert and cert_inhabited supply a concrete witness so downstream code can assume the certificate without rebuilding the inequalities.

why it matters in Recognition Science

Gives Foundation a named, inhabitable certificate that wave-particle duality is read off the same $J$-cost that forces $\phi$, the eight-tick octave, and $D=3$, rather than postulated as an independent quantum axiom. No downstream used_by edges are recorded yet, so the module is a leaf certificate: available for later forcing-chain or measurement-layer theorems that need a three-regime duality hypothesis in Type form. Ties to T5 ($J$-uniqueness) and, by naming, to the three-dimensional spatial claim (T8) without re-proving either here.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (8)