`derivedCost`

definition

show as: view math explainer →

module: IndisputableMonolith.Foundation.LogicAsFunctionalEquation
domain: Foundation
line: 69 · github
papers citing: 7 papers (below)

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Foundation.LogicAsFunctionalEquation on GitHub at line 69.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

  66/-- The cost function derived from a comparison operator by fixing the
  67second argument at the multiplicative identity. Under scale invariance,
  68this is well-defined on the multiplicative group of positive ratios. -/
  69@[simp] def derivedCost (C : ComparisonOperator) : ℝ → ℝ :=
  70  fun r => C r 1
  71
  72/-! ## The Four Aristotelian Constraints
  73
  74We encode the classical laws of logic as structural constraints on a
  75comparison operator. The mapping from Aristotle's propositional
  76formulations to functional constraints on C is:
  77
  78  Identity (A = A)             ↦  C(x, x) = 0
  79                                  comparison of a thing with itself is trivial
  80  Non-contradiction (¬(A ∧ ¬A))↦  C(x, y) = C(y, x)
  81                                  the cost is single-valued under reordering
  82                                  (with scale invariance, this gives reciprocity
  83                                   F(x) = F(1/x))
  84  Excluded middle (A ∨ ¬A)     ↦  C is continuous and total on its domain
  85                                  every comparison returns a definite value
  86  Composition consistency      ↦  Route-independence (the d'Alembert form)
  87                                  comparisons assembled forward and backward
  88                                  must compose by a fixed combining rule
  89-/
  90
  91/-- **Identity**: comparing a thing with itself costs zero. The mathematical
  92counterpart of the Aristotelian law A = A. -/
  93def Identity (C : ComparisonOperator) : Prop :=
  94  ∀ x : ℝ, 0 < x → C x x = 0
  95
  96/-- **Non-contradiction (reciprocal symmetry)**: the cost of comparing x to y
  97equals the cost of comparing y to x. The mathematical counterpart of the
  98Aristotelian law ¬(A ∧ ¬A): if comparison were not single-valued under
  99reordering, the same comparison would simultaneously hold and not hold. -/

papers checked against this theorem (showing 7 of 7)

State-space models align semantics across point cloud batches
unclear · 2605.01759

"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
unclear · 2605.01659

"RREP = exp(−(1/N) Σ min_{t'∈S} |H_t − H_{t'}|)"
Multi-scale features train SDF to detect 3D point cloud anomalies
unclear · 2605.03437

"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
unclear · 2605.03056

"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
unclear · 2605.02365

"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
unclear · 2605.02471

"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
unclear · 2605.03196

"we compute each prompt's own_dist — cosine distance to its form's A-only centroid — as the reliability score."