IndisputableMonolith.Foundation.ExistenceUniquenessFromCost
This module proves the cost function vanishes only at 1. Researchers deriving uniqueness of the self-similar fixed point from the Recognition Science functional equation would cite it. The argument assembles symmetry and isolation lemmas on the J-cost into singleton and one-member properties for the zero set, then packages them as an ExistenceUniquenessCert.
claimThe zero set of the cost function satisfies $Z = {x > 0 | cost(x) = 0} = {1}$.
background
The module imports the RS-native time quantum τ₀ = 1 tick from Constants and the cost function from the Cost module. It defines supporting lemmas including jcost_log_symmetric (J-cost invariance under x ↔ 1/x) and jcost_isolated_from_zero (J-cost bounded away from zero for x ≠ 1). These establish the local setting in which cost properties imply existence and uniqueness for solutions of the underlying functional equation.
proof idea
The module organizes its content as a chain of lemmas: jcost_log_symmetric and jcost_isolated_from_zero supply the algebraic and isolation facts; cost_zero_set_singleton and cost_zero_set_has_one_member convert them into set statements; these are assembled into the ExistenceUniquenessCert and its constructor existenceUniquenessCert. No single tactic block; the structure is lemma composition.
why it matters in Recognition Science
This module supplies the cost-zero singleton property that feeds ExistenceUniquenessCert inside the same module. It fills the step from the cost definition to uniqueness of the fixed point required by the forcing chain at T5 (J-uniqueness). It touches the derivation of all constants from the single Recognition Composition Law.
scope and limits
- Does not define the cost function (imported from Cost).
- Does not extend the result to non-positive reals.
- Does not derive numerical values for G, ħ or α.
- Does not address the eight-tick octave or D = 3.