public_cost_layer
plain-language theorem explainer
The theorem asserts that the public cost layer holds, packaging J-uniqueness on positives, the cosh closed form, symmetry, nonnegativity, zero condition at unity, and the null barrier. Researchers citing the dimensional-constraints rebuttal reference this compact interface. The proof constructs the structure record by direct substitution of the primitive-to-uniqueness lemma together with the core Jcost identities.
Claim. The cost functional satisfies: for any admissible primitive cost functional $F$ with Aczel regularity kernel, $F(x) = J(x)$ on $x > 0$; $J(x) = J(x^{-1})$; $J(x) = (x-1)^2/(2x) = 0$ iff $x=1$; $J(x) = 0$ at $x=1$; $J(x) = 0$ implies $x=1$; and the null barrier that nothing cannot exist. Equivalently, in logarithmic coordinates $J(e^t) = e^t + e^{-t} - 2$.
background
PublicCostLayer is the structure that collects the minimal cost properties required for the dimensional-constraints rebuttal. Its fields are uniqueness on positives via the primitive-to-uniqueness route, the logarithmic closed form $Jlog t = cosh t - 1$, normalization at unity, reciprocity, nonnegativity, the zero-iff-unity condition, and the null barrier. Jcost itself is defined as the squared ratio $(x-1)^2/(2x)$ for $x > 0$, which is nonnegative by AM-GM and symmetric under inversion. The module packages these statements in a public namespace without importing the full confidential development.
proof idea
The term proof refines a PublicCostLayer record. The unique_on_pos field is supplied by primitive_to_uniqueness_of_kernel applied to the functional-equation hypotheses. log_closed_form is filled by Jlog_as_cosh. normalized uses Jcost_unit0. reciprocal uses Jcost_symm. nonnegative uses Jcost_nonneg. zero_iff_one uses Jcost_eq_zero_iff. null_barrier uses nothing_cannot_exist from the law of existence.
why it matters
This result supplies the public cost-theoretic core for the dimensional-constraints rebuttal, assembling the T5 J-uniqueness property and its immediate consequences into a single interface. It sits downstream of the cost algebra and Aczel classification lemmas and supports the framework's derivation of physics from the single functional equation. No open scaffolding remains; the declaration is fully proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.