IndisputableMonolith.Foundation.DAlembert.AnalyticBridge
This module supplies the log-lift of a cost function as the analytic bridge inside the d'Alembert development. Researchers formalizing RCL necessity cite it to connect cost metrics to the curvature and entanglement gates. The module organizes the argument by importing Cost, NecessityGates, EntanglementGate, and CurvatureGate without internal proofs.
claimThe log-lift $G(t) = F(e^t)$ of a cost function $F$, equipped with the 1D metric $ds^2 = G''(t) dt^2$ and the cross-derivative condition on the combiner $P$.
background
The module resides in Foundation.DAlembert and imports Cost together with three gate modules. CurvatureGate states that the cost metric must have constant nonzero curvature, realized by the log-coordinate representation $G(t) = F(e^t)$ with $ds^2 = G''(t) dt^2$. EntanglementGate requires the combiner $P$ to satisfy $\partial^2 P / \partial u \partial v eq 0$. NecessityGates records that symmetry, normalization, $C^2$ regularity, calibration, and existence of some $P$ do not force the d'Alembert/RCL structure, as shown by the counterexample in Counterexamples.lean. The module doc comment identifies its central object as the log-lift of a cost function.
proof idea
This is a definition module, no proofs.
why it matters in Recognition Science
The module supplies the analytic bridge that feeds the curvature and entanglement characterizations into the necessity argument for the Recognition Composition Law. It directly supports the d'Alembert development whose parent results appear in the NecessityGates and CurvatureGate modules. No used_by edges are recorded, indicating it functions as an internal connector rather than a terminal theorem.
scope and limits
- Does not contain the main RCL inevitability theorems.
- Does not discharge the counterexample in NecessityGates.
- Does not define the full forcing chain T0-T8.
- Does not compute numerical constants such as alpha or G.
depends on (4)
declarations in this module (24)
-
def
G_of -
def
H_of -
theorem
log_consistency -
theorem
G_zero -
theorem
Q_boundary_v -
theorem
Q_boundary_u -
lemma
separable_forces_additive -
theorem
separable_forces_flat_ode -
theorem
entangling_forces_hyperbolic_ode -
theorem
flat_ode_unique -
theorem
hyperbolic_ode_unique -
theorem
even_function_deriv_zero -
theorem
separable_combiner_forces_flat -
theorem
entangling_combiner_forces_hyperbolic -
theorem
differentiation_key_lemma -
theorem
entangling_with_boundary_is_RCL -
theorem
analytic_bridge -
theorem
analytic_bridge_full -
theorem
Jcost_satisfies_dAlembert -
theorem
F_forced_to_Jcost -
theorem
P_forced_to_RCL -
theorem
full_inevitability -
theorem
gates_connected -
theorem
Jcost_has_RCL_combiner