Pith. sign in
module module moderate

IndisputableMonolith.Foundation.WaveParticleDuality3FromJCost

show as:
view Lean formalization →

Foundation module that packages wave–particle duality in three spatial dimensions as a consequence of the J-cost. It defines a domain cost, a positive canonical threshold, and an inhabited certificate WPDuality3Cert. Cite it when linking T5 J-uniqueness and T8 (D=3) to dual propagation modes. The argument is definitional plus nonnegativity and threshold positivity lemmas, not a deep tactic proof.

claimFrom the J-cost $J(x)=(x+x^{-1})/2-1$, the module introduces a domain cost $C$ on admissible domains, a canonical threshold $\theta>0$, and a certificate that wave-like and particle-like regimes are dual in $D=3$ once $C$ crosses $\theta$. Nonnegativity $C\ge 0$ and equality-at-identity facts are recorded alongside an inhabited certificate type.

background

Recognition Science forces the cost functional $J$ uniquely (T5) by the Recognition Composition Law, and forces three spatial dimensions (T8). Wave–particle duality is read as two regimes of the same cost: extended (wave) versus localized (particle) recognition, separated by a threshold on a domain-level cost built from $J$.

The module sits in Foundation and imports Constants (RS-native units, including the tick $\tau_0$) and Cost (the $J$-cost API). Sibling definitions supply domainCost (cost assigned to a domain), its value at the identity configuration, nonnegativity, a canonicalThreshold with a positivity lemma, and the certificate bundle WPDuality3Cert with an inhabited instance cert.

Local setting: derive a 3D duality statement from $J$ alone, without extra dynamical postulates, so later layers can treat wave and particle channels as cost regimes rather than independent ontologies.

proof idea

Definition-heavy module. It introduces domainCost and proves elementary facts (domainCost_at_eq, domainCost_nonneg) by unfolding $J$ and using standard inequalities. canonicalThreshold is defined and shown positive (canonicalThreshold_pos). The certificate type WPDuality3Cert packages the duality claim in $D=3$; cert and cert_inhabited supply a concrete inhabitant so downstream code can assume the certificate without reconstructing the threshold argument. No long tactic scripts: structure is defs plus short positivity/equality lemmas.

why it matters in Recognition Science

Connects T5 (unique $J$) to T8 ($D=3$) by giving an explicit cost-threshold reading of wave–particle duality. Downstream used-by edges are empty in the graph snapshot, so this module is a leaf certificate provider: other Foundation or phenomenology layers can import WPDuality3Cert rather than re-derive the threshold. It keeps duality inside the forcing chain instead of as an external quantum postulate. Open follow-ons would attach concrete mass-ladder or eight-tick timing bounds to the same threshold; those are outside this file.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (8)