Materials Fiber Reinforcement3 From Jcost

Fiber reinforcement and the ledger

Fiber-reinforced composites combine stiff fibers with a softer matrix to get a material stronger than either part alone. The classic rule of mixtures estimates the composite's stiffness as a weighted average: E_composite = E_fiber * Vf + E_matrix * (1-Vf), where Vf is the volume fraction of fibers. The question is what fraction to choose. Too little fiber and the matrix carries the load; too much and the fibers cannot bond properly. The rule of mixtures itself does not pick an optimum.

In Recognition Science, the framework's cost function J(x) = (x + 1/x)/2 - 1 measures the price of a mismatch between two quantities. Applied to fiber and matrix, the framework models the ideal fiber fraction as the point where the cost of recognizing the fiber against the matrix is balanced. The research note in the module records the intended result: an optimal volume fraction of Vf = J(phi) = 0.118, or 11.8 percent fiber, where phi is the golden ratio. That number is a research note, not a theorem.

The machine-checked library of formal theorems proves three general facts about the cost function J(x): it equals zero when its two inputs are equal, it is never negative for positive inputs, and the threshold phi - 3/2 is positive. These are properties of J itself, not of any composite material. The module defines its material cost as J(m/e) without specifying what m and e mean in fiber terms, so the proofs establish nothing specific to fiber reinforcement.

The honest reading: the module is a template. It shows that a cost function with the right shape has certain universal properties, and it records where a material-specific definition was meant to go. What would turn it into a theorem about composites is a definition of m and e in terms of fiber and matrix properties. That definition does not yet exist in the module, so the 11.8 percent figure remains an unproven research note, not a derived result.

def domainCost (m e : ℝ) : ℝ := Jcost (m / e)

def domainCost (m e : ℝ) : ℝ := Jcost (m / e)

theorem domainCost_at_eq (r : ℝ) (h : r ≠ 0) : domainCost r r = 0 := by
  unfold domainCost; rw [div_self h]; exact Jcost_unit0

theorem domainCost_nonneg (m e : ℝ) (hm : 0 < m) (he : 0 < e) : 0 ≤ domainCost m e := by
  unfold domainCost; exact Jcost_nonneg (div_pos hm he)

theorem canonicalThreshold_pos : 0 < canonicalThreshold := by
  unfold canonicalThreshold; linarith [phi_gt_onePointFive]

def domainCost (m e : ℝ) : ℝ := Jcost (m / e)

def domainCost (m e : ℝ) : ℝ := Jcost (m / e)

What this page does not claim

The module proves the 11.8 percent fiber fraction is optimal for any real composite. The rule of mixtures is derived from the cost function J. The framework's cost function has been shown to govern actual fiber-matrix interactions.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Materials/Fiber_Reinforcement3_FromJCost.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: