pith. sign in
module module high

IndisputableMonolith.NumberTheory.ZeroCompositionInterface

show as:
view Lean formalization →

The ZeroCompositionInterface module supplies the abstract zero-location composition law required by the Vector C symmetry analysis in Recognition Science. Researchers assembling the RH bridge from cost uniqueness through analytic trace would cite it as the interface layer. The module assembles definitions from the functional equation and zero location cost imports without containing proofs.

claimThe abstract zero-location composition law $ZeroCompositionLaw$ relating zeroDefect$( ho)$ and zeroDefect$(ar{ ho})$ via the J-functional on deviations $2( ext{Re } ho - 1/2)$.

background

This module resides in the NumberTheory domain. It imports the FunctionalEquation module, which supplies lemmas for the T5 cost uniqueness proof, and the DiscretenessForcing module, whose doc states: "discreteness is forced by the cost landscape" with J(x) = ½(x + x⁻¹) - 1 having unique minimum at x = 1 and J(e^t) = cosh(t) - 1. The ZeroLocationCost module supplies the dictionary zeroDeviation ρ = 2(Re ρ - 1/2) and zeroDefect ρ = defect(exp(zeroDeviation ρ)).

The module provides the abstract interface for the composition law on zero defects needed downstream.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The module feeds AnalyticTrace, which assembles the full RH bridge and has eliminated prior axioms, and VectorCSymmetryOnlyNoGo, whose doc states it "formalizes the main stage gate for Vector C" by showing reflection plus conjugation symmetries give pairing data but do not force the critical line. It supplies the missing abstract zero-location composition law for that gate.

scope and limits

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (3)

Lean names referenced from this declaration's body.

declarations in this module (8)