additive_strict_of_both_inconsistent
For a cost function obeying dichotomy and independent additivity, the cost of an independent join of two inconsistent configurations strictly exceeds each separate cost. Recognition Science researchers working on the T-1 to T0 bridge would cite this to obtain quantitative structure from the recognition-work constraint. The proof is a direct term-mode reduction: additivity supplies the sum equality, cost_pos_of_inconsistent supplies the two strict inequalities, and linarith finishes the conjunction.
claimLet $κ$ be a cost function on a configuration space that satisfies the dichotomy axiom (cost zero if and only if the configuration is consistent) and independent additivity. For any two independent configurations $Γ_1$ and $Γ_2$ that are both inconsistent, the cost of their join satisfies $κ.C( join(Γ_1, Γ_2) ) > κ.C(Γ_1)$ and $κ.C( join(Γ_1, Γ_2) ) > κ.C(Γ_2)$.
background
The module formalizes the recognition-work constraint theorem by introducing a cost function on an abstract configuration space. A configuration space supplies a join operation and an independence relation (configurations share no predicates). The CostFunction structure encodes two axioms: (D) dichotomy, stating that cost is zero precisely on consistent configurations, and (A) independent additivity, stating that cost of a join equals the sum of the costs when the configurations are independent. The upstream lemma cost_pos_of_inconsistent converts the negation of consistency into a strict positivity statement for the cost value.
proof idea
The term proof first applies the additivity field of the CostFunction instance to obtain the equality κ.C(join Γ₁ Γ₂) = κ.C Γ₁ + κ.C Γ₂. It then invokes cost_pos_of_inconsistent twice, once for each input configuration, to produce the two strict inequalities 0 < κ.C Γ₁ and 0 < κ.C Γ₂. The final refine step packages the two linarith applications into the required conjunction.
why it matters in Recognition Science
The result supplies the strict inequality needed to turn the additive decomposition into a genuine quantitative cost measure on composite configurations. It directly supports the module's claim that independent additivity plus the satisfiability dichotomy forces the cost function to be uniquely determined by its values on indecomposable inconsistent generators. Within the Recognition Science chain this step closes the gap between the naming of recognition work and the emergence of additive structure on the phi-ladder.
scope and limits
- Does not establish additivity when the configurations are dependent.
- Does not provide a lower bound on the cost difference beyond strict inequality.
- Does not apply when either configuration is consistent.
- Does not address finite joins of more than two configurations.
formal statement (Lean)
216theorem additive_strict_of_both_inconsistent (κ : CostFunction Config)
217 (Γ₁ Γ₂ : Config)
218 (h_indep : Independent Γ₁ Γ₂)
219 (h₁ : ¬IsConsistent Γ₁) (h₂ : ¬IsConsistent Γ₂) :
220 κ.C (join Γ₁ Γ₂) > κ.C Γ₁ ∧ κ.C (join Γ₁ Γ₂) > κ.C Γ₂ := by
proof body
Term-mode proof.
221 have h_eq : κ.C (join Γ₁ Γ₂) = κ.C Γ₁ + κ.C Γ₂ :=
222 κ.additivity Γ₁ Γ₂ h_indep
223 have h₁_pos : 0 < κ.C Γ₁ := cost_pos_of_inconsistent κ Γ₁ h₁
224 have h₂_pos : 0 < κ.C Γ₂ := cost_pos_of_inconsistent κ Γ₂ h₂
225 refine ⟨?_, ?_⟩
226 · linarith
227 · linarith
228
229/-- Cost is additive over independent join with the empty configuration
230(degenerate case of independent additivity). -/