Hugging Face's logo

Snapkitty
/
hcalc

snapkitty
october-2026-drop
lean4
alloy
j
dynamical-systems
contraction
formal-verification
research
Model card Files
xet
 Community
hcalc / lean /README.md
SNAPKITTYWEST's picture
SNAPKITTYWEST
October 2026 main drop: mirror from GitHub
d7b24f0 verified
preview code
|
Raw History Blame Contribute Delete
3.24 kB

HCALC Lean 4 formalization (PRODUCTION)

License: AGPL-3.0-only (see LICENSE)
Copyright (C) 2026 HCALC contributors

Production formalization of the HCALC nested recurrence

[ X_{t+1} = \Xi\bigl(t,; \Lambda_m \cdot C(T_p(X_t))\bigr) ]

frozen to Spec ../spec/PRODUCTION.md (overrides provisional L6 axioms in COHERENCE/AXIOMS).

Provenance

Part Source
Carrier, Tp Ξ±-diag, C softScale-or-id, Ξ›m min-formula, Ξ=ΞΎy+g, J=residual, L5 Hyp, L7 InstanceBridge Spec-file PRODUCTION.md
Option B InstanceBridge (not NestedFaithful / not rfl) Spec-file PRODUCTION.md Β§6 (f5a08da)
Mathlib ℝ (thin bridge in RealStub) Mathlib4 v4.34.1
Foundry L1–L4 (P64, Gershgorin, FoundryStep additive, softProject schedules) Spec + Foundry PROPERTIES (FoundryAdditive distinct)

Mathlib

  • Toolchain: leanprover/lean4:v4.34.1 (matches Mathlib tag v4.34.1 lean-toolchain β€” no bump needed).
  • Dependency: leanprover-community/mathlib @ v4.34.1.
  • Imports used (minimal):
    1. Mathlib.Basic.Real.Basic β€” ℝ, field/order/abs/min/max
    2. Mathlib.Analysis.SpecialFunctions.Log.Basic β€” Real.log (pulls Exp; Topology transitive only)
    • finMax uses core Fin.foldl only (no Finset / Mathlib.Data.Fin)
  • No Topology / MeasureTheory / aesop / grind / large simp sets.
  • Proofs are freehand calc / rw / intro / apply / elementary single-lemma exact.

finMax / β„“βˆž

finMax = Fin.foldl of max with init 0 (smallest surface; not Finset.univ.sup' / iSup). Production sites pass nonnegative args (|Β·|, Gershgorin disks); n = 0 yields 0.

Layout

File Role
Hcalc/RealStub.lean Thin Mathlib ℝ re-exports + freehand Real lemmas (finMax, softScale, guards)
Hcalc/Carrier.lean Gap-Carrier CLOSED: Carrier n := Fin n β†’ ℝ, β„“βˆž
Hcalc/Foundry.lean L1–L4 defs; FoundryAdditive FoundryStep (β‰  nested); Gap-Foundry-* may remain
Hcalc/Axioms.lean L6 defs Tp/C/Ξ›m/Ξ/J/ContractAlg + L7 InstanceBridge
Hcalc/Pipeline.lean Nested hcalcStep / step / J / optimize
Hcalc/Convergence.lean L5 unique FP + residual under HypContractive
Hcalc/Invariants.lean Structural invariants
Hcalc/Production.lean Stable re-exports for Verify/docs

Rules

  • Zero sorry / admit.
  • Production Gap-* are defs/theorems, not opaque axioms.
  • Gap-Real-arith for Real itself is closed (Mathlib ℝ). Gap-Foundry-* stubs OK if Foundry.State stays opaque.
  • L7 = InstanceBridge Option B (parameter table + toFoundryStep diagnostic). Not FoundryStep = hcalcStep.
  • C is state softScale-or-id; does not equal Foundry softProject on (Ξ,Ξ›) schedules.
  • Ξ± (Tp weights) is Spec-only.
  • No unconditional convergence β€” L5 under HypContractive only.

Build 

source ~/.elan/env
cd /workspace/hcalc/lean
lake update          # first time / after mathlib pin change
lake exe cache get    # download Mathlib oleans (recommended)
lake build 2>&1 | tee build.log

Toolchain: leanprover/lean4:v4.34.1 + Mathlib v4.34.1.