derivedCost
plain-language theorem explainer
derivedCost extracts the single-variable cost function F(r) = C(r, 1) from any comparison operator C on positive reals. Researchers deriving the Recognition Composition Law or the continuous-combiner classification cite it when reducing two-argument comparisons to a scale-invariant cost on ratios. The definition is a direct projection that fixes the second argument at the multiplicative identity.
Claim. Let $C : (0,∞) × (0,∞) → ℝ$ be a comparison operator. The derived cost is the function $F : (0,∞) → ℝ$ defined by $F(r) := C(r, 1)$.
background
ComparisonOperator is the type of maps from pairs of positive reals to reals that return the cost of comparing two quantities. The module encodes the four Aristotelian constraints (identity, non-contradiction, excluded middle, composition consistency) as structural properties on such operators. Under scale invariance the derived cost is well-defined on the multiplicative group of positive ratios.
proof idea
The definition is a one-line projection: derivedCost C is the function sending r to C r 1. No lemmas or tactics are invoked; the body is the direct extraction of the cost by fixing the second argument at 1.
why it matters
This definition supplies the cost function F that appears in generatorOfLawsOfLogic to extract a non-trivial generator from SatisfiesLawsOfLogic. It is the input to the continuous-combiner theorems in GeneralizedDAlembert (bilinear classification, log-smoothness bootstrap, finite-smoothness promotion). In the Recognition framework it converts the Aristotelian laws into the functional equation whose solution yields the J-cost and the phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.
papers checked against this theorem (showing 7 of 7)
-
State-space models align semantics across point cloud batches
"L_SPD = (1/N) Σ ||f_s_i − f_t_i||²₂ ; L_fine-tune = L_task + λ_SPD L_SPD + λ_geo L_geo"
-
Entropy-based RL matches supervised video summarization
"RREP = exp(−(1/N) Σ min_{t'∈S} |H_t − H_{t'}|)"
-
Multi-scale features train SDF to detect 3D point cloud anomalies
"L_SDF = (1/Card(P~)) Σ (d~_i − d*_i)^2 ... The absolute value of d~ ... directly serves as the anomaly score"
-
PINN cuts qubit gate times 20-40% at 99% fidelity
"H_eff(t) = h_z(t)σ_z + h_x(t)σ_x with h_z = J23/4 − J12/2, h_x = √3 J23/4; pulse shapes optimized by a 4-layer tanh PINN"
-
Neural approximation yields periodic paths along brain heteroclinic cycles
"Universal Approximation Theorem used to approximate an arbitrary smooth vector field by −x + Pσ(Wx+b)"
-
Unpaired super-resolution yields 54% Dice in dead tree segmentation
"L_ADA-Net = L_A + λ L_Spatial + β L_IDSpatial + γ L_Freq + ϑ L_IDFreq (adversarial + contrastive losses with tuned weights)"
-
Unanswerable math prompts deviate in LLM geometry before output
"we compute each prompt's own_dist — cosine distance to its form's A-only centroid — as the reliability score."