Primitive Axiomatics of Finite Obstruction Calculus

{"Title":[0],"Primitive":[1],"Axiomatics":[2],"of":[3,265,471,635],"Finite":[4,187,366,404],"Obstruction":[5],"Calculus":[6],"Subtitle":[7],"Evaluation":[8,85],"Preorders,":[9],"Quotient":[10,528],"Residuals,":[11],"Closure":[12,467,564,571,586],"Charge,":[13],"and":[14,30,47,65,102,126,146,170,174,210,308,362,369,382,477,507,672,739],"Observer-Selected":[15],"Geometry":[16],"Abstract":[17],"For":[18],"a":[19,25,31,40,44,48,90,95,183,221,261],"finite":[20,62,96,154,161,175,222,407],"directed":[21],"evaluation":[22,78,188,470],"carrier":[23,93],"with":[24,179,289,400,418,496,516],"chosen":[26,91],"2-truncated":[27],"cochain":[28,97,408],"complex":[29],"scalar":[32,142,155],"observer":[33,180,367,670],"gauge,":[34,271],"every":[35],"observed":[36,267],"edge":[37],"inconsistency":[38,88,235,268],"carries":[39],"quotient":[41,99,118,228,324,430],"residual":[42,100,119,243,252,431],"class,":[43],"closure":[45,82,104,124,256,319,472,478],"charge,":[46,125],"bounded":[49],"obstruction":[50,63,111,253],"signature":[51,112],"(Φ₁,":[52,113,685],"Γ₂,":[53,114,686],"R_{cl}).":[54],"This":[55,218],"paper":[56,219,280],"states":[57],"the":[58,110,140,153,227,461,641,752],"primitive":[59],"axiomatics":[60],"for":[61,224,691],"calculus":[64,178],"separates":[66,234,250],"proved":[67],"structure":[68,364],"from":[69,241,254,644],"observer-dependent":[70],"assumptions.":[71],"Local":[72],"comparison":[73],"is":[74,83,109,133,137,260,662,666,751],"modeled":[75],"by":[76,139,237,684],"an":[77,84,282],"relation":[79],"whose":[80],"reflexive-transitive":[81],"Preorder.":[86],"Pairwise":[87],"over":[89,465],"simplicial":[92,165],"gives":[94,220],"complex,":[98],"space,":[101],"descended":[103],"map.":[105],"The":[106,258,279,744],"core":[107],"diagnostic":[108,223],"R_{cl}):":[115],"Φ₁":[116,452],"measures":[117,122],"mass,":[120],"Γ₂":[121,474],"d₁":[123,248,417,421,575],"R_{cl}":[127],"records":[128],"their":[129],"ratio.":[130],"Metric":[131],"magnitude":[132],"not":[134],"universal;":[135],"it":[136],"selected":[138],"observer's":[141],"gauges,":[143],"aggregation":[144,306],"law,":[145],"compatible":[147],"transformation":[148],"monoid.":[149],"Sections":[150,157],"§1.0–§1.10":[151],"establish":[152],"core;":[156],"§2.0–§2.4":[158],"develop":[159],"explicit":[160],"extensions":[162],"including":[163],"arbitrary-degree":[164],"cohomology,":[166],"discrete":[167,284],"mathematical":[168],"physics":[169],"combinatorial":[171],"conservation":[172],"laws,":[173],"quantum":[176,636],"trace-norm":[177],"passivity.":[181],"Why":[182],"Researcher":[184],"Should":[185],"Care":[186],"systems":[189],"often":[190],"produce":[191],"local":[192,238],"comparisons":[193],"that":[194,225,659],"cannot":[195],"be":[196],"globally":[197],"reconciled":[198],"—":[199,269],"constraint":[200],"solvers,":[201],"distributed":[202],"logs,":[203],"model-evaluation":[204],"traces,":[205],"sensor":[206],"networks,":[207],"proof-search":[208],"attempts,":[209],"multi-agent":[211],"review":[212],"pipelines":[213],"all":[214],"have":[215],"this":[216],"shape.":[217],"failure:":[226],"Q¹":[229,326,581],"=":[230,247,327,424,434,444,451,453,475,481,535,547,558,567,574,582,592],"C¹":[231,328,562,583],"/":[232,329,521,584,594],"im(d₀)":[233,330,585],"removable":[236,270],"reference":[239],"changes":[240],"irreducible":[242],"obstruction,":[244,273],"while":[245],"κ¹([h])":[246,573],"h":[249,576],"closed":[251,272],"active":[255],"failure.":[257],"payoff":[259],"replayable":[262],"three-way":[263],"classification":[264],"any":[266],"or":[274,640,651,680,734],"non-closed":[275],"rupture.":[276],"System":[277],"Architecture":[278],"integrates":[281],"exact":[283,333],"rational":[285],"solver":[286],"in":[287,302,394,749],"Python":[288,388,396,699],"9":[290,724],"sorry-free":[291],"Lean":[292,297,715],"4":[293,298,716],"formalization":[294],"modules:":[295],"A.":[296],"Formalization":[299],"Layer":[300],"(primitive_axiomatics":[301],"lean4)":[303],"Core.lean:":[304],"Root":[305],"module":[307],"formal":[309],"exports":[310],"TriangleReplay.lean:":[311],"Worked":[312],"cyclic":[313],"2-simplex":[314],"example":[315],"replay":[316],"KappaWellDefined.lean:":[317],"Descended":[318,570],"map":[320],"κ¹":[321],"well-defined":[322,579],"on":[323,580,669],"space":[325],"ExactSequence.lean:":[331],"Short":[332],"sequence":[334],"0":[335,343,425,589,600,608],"→":[336,338,340,342,601,603,607],"H¹(P)":[337,602],"Q¹(P)":[339,604],"im(d₁)":[341,606],"ClosureRatioBound.lean:":[344],"Exact":[345,386,406,428,438,598],"operator":[346],"norm":[347],"bound":[348,371,748],"R_cl":[349,480],"≤":[350,357,373,375,447,554,590,596,613,620,622,624,626],"‖d₁‖₁→₁":[351],"ObserverPassivity.lean:":[352],"Observer":[353,360,609,615],"non-creation":[354],"inequality":[355],"Φ_O(O(q))":[356,612],"Φ(q)":[358,614],"ObserverFamilyPoset.lean:":[359],"poset":[361],"refinement":[363],"GrammarBound.lean:":[365],"resolution":[368],"vocabulary":[370],"|Q¹_G|":[372,619],"|im(r)|":[374,621],"|G|":[376,623],"ConstructorIncrement.lean:":[377],"Minimal":[378],"increment":[379],"initiality":[380],"boundary":[381],"inductive":[383],"preservation":[384],"B.":[385],"Rational":[387],"Replay":[389],"Engine":[390],"(code/l000_replay.py)":[391],"Implemented":[392],"strictly":[393,667],"pure":[395],"standard":[397,727],"library":[398],"(`fractions.Fraction`)":[399],"zero":[401,505],"floating-point":[402],"approximation:":[403],"Complexes:":[405],"spaces":[409],"C⁰,":[410],"C¹,":[411],"C²":[412],"Coboundaries:":[413],"Boundary":[414],"operators":[415],"d₀,":[416],"verified":[419],"nilpotence":[420],"∘":[422],"d₀":[423,540],"Primal":[426,458],"Optimization:":[427],"ℓ¹":[429,665],"minimization":[432],"(Φ₁":[433],"2)":[435,454],"Dual":[436,532],"Certificate:":[437,533],"dual":[439,462,503],"witness":[440,463],"verification":[441],"(d₀*":[442],"ψ":[443,557,560],"0,":[445,559],"‖ψ‖_∞":[446,553],"1,":[448,555],"⟨ψ,":[449,550],"δ⟩":[450,551],"Zero":[455],"Duality":[456],"Gap:":[457],"optimum":[459],"matches":[460],"certificate":[464,682],"ℚ":[466],"Invariants:":[468],"Direct":[469],"charge":[473],"2":[476],"ratio":[479],"1":[482],"C.":[483],"Test":[484,488],"Suite":[485,489],"&":[486,526,531,631,697],"Verification":[487,698],"(code/test_l000_replay.py):":[490],"81":[491],"unit":[492],"test":[493],"cases":[494],"passing":[495],"99%":[497],"branch":[498],"coverage":[499,712],"(verifying":[500],"nilpotency,":[501],"optimality,":[502],"witnesses,":[504],"gap,":[506],"gauge":[508,653],"invariance)":[509],"Reviewer":[510],"Notebook":[511,731],"(jupyter_notebooks/001_reviewer_primitive_axiomatics.ipynb):":[512],"Interactive":[513],"inspection":[514],"sandbox":[515],"headless":[517],"launch":[518],"scripts":[519],"(`public_export/run_notebook.bat`":[520],"`.sh`)":[522],"Key":[523],"Closed":[524],"Forms":[525],"Formulations":[527],"Residual":[529],"Magnitude":[530],"Φ₁([δ])":[534],"inf":[536],"{":[537,549],"‖δ":[538],"-":[539],"f‖₁":[541],":":[542,552],"f":[543],"∈":[544,561,577],"C⁰":[545],"}":[546,563],"max":[548],"d₀*":[556],"Charge:":[565],"Γ₂(δ)":[566],"‖d₁":[568],"δ‖₁":[569],"Map:":[572],"im(d₁),":[578],"Ratio":[587],"Bound:":[588,618],"R_{cl}([h])":[591],"Γ₂(h)":[593],"Φ₁([h])":[595],"‖d₁‖_{1→1}":[597],"Sequence:":[599],"→(κ¹)":[605],"Passivity":[610],"(No-Creation):":[611],"Grammar":[616],"Resolution":[617],"∑_{ℓ":[625],"L}":[627],"|Σ|^ℓ":[628],"Negative":[629],"Scopes":[630],"Non-Claims":[632],"No":[633,646,656,675],"derivation":[634],"mechanics,":[637],"Hilbert":[638],"spaces,":[639],"Born":[642],"rule":[643],"Φ₁.":[645],"Lorentz":[647],"invariance,":[648],"spacetime":[649],"relativity,":[650],"physical":[652],"coupling":[654],"constants.":[655],"universal":[657],"claim":[658],"metric":[660],"geometry":[661],"fundamentally":[663],"ℓ¹;":[664],"conditional":[668],"symmetry":[671],"replica-extensivity":[673],"axioms.":[674],"autonomous":[676],"promotion,":[677],"moral":[678],"authority,":[679],"legal":[681],"conferred":[683],"R_{cl})":[687],"alone.":[688],"See":[689],"`docs/nonclaims.md`":[690],"complete":[692],"scope":[693],"fences.":[694],"Cold":[695],"Reproduction":[696],"Tests:":[700],"python":[701,742],"-m":[702],"unittest":[703],"discover":[704],"-s":[705],"code":[706],"-p":[707],"\\"test_*.py\\"":[708],"(81":[709],"passed;":[710],"statement":[711],">=":[713],"99%).":[714],"Build:":[717],"cd":[718],"lean4":[719],"&&":[720],"lake":[721],"build":[722],"(all":[723],"modules":[725],"sorry-free;":[726],"kernel":[728],"axioms":[729],"only).":[730],"Launcher:":[732],"public_export/run_notebook.bat":[733],"public_export/run_notebook.sh.":[735],"Publication":[736],"PDF:":[737],"Source-buildable":[738],"content-equivalent":[740],"via":[741],"scripts/build_paper_artifacts.py.":[743],"submitted":[745],"primitive_axiomatics.pdf":[746],"(SHA-256":[747],"SHA256SUMS)":[750],"authoritative":[753],"publication":[754],"rendering.":[755]}

Authors

Publication Details

Journal
Zenodo (CERN European Organization for Nuclear Research)
Published
2026-09-21
DOI
https://doi.org/10.5281/zenodo.22883358
Primary Topic
Logic, Reasoning, and Knowledge
Type
preprint
Controls
|||
ALL TIME
JAN
FEB
MAR
APR
MAY
JUN
JUL
AUG
SEP
preprint

Primitive Axiomatics of Finite Obstruction Calculus

Jeremy H. Carroll
Zenodo (CERN European Organization for Nuclear Research)
Logic, Reasoning, and Knowledge
preprint

Primitive Axiomatics of Finite Obstruction Calculus

Jeremy H. Carroll
preprint en

Abstract

Title Primitive Axiomatics of Finite Obstruction Calculus Subtitle Evaluation Preorders, Quotient Residuals, Closure Charge, and Observer-Selected Geometry Abstract For a finite directed evaluation carrier with a chosen 2-truncated cochain complex and a scalar observer gauge, every observed edge inconsistency carries a quotient residual class, a closure charge, and a bounded obstruction signature (Φ₁, Γ₂, R_{cl}). This paper states the primitive axiomatics for finite obstruction calculus and separates proved structure from observer-dependent assumptions. Local comparison is modeled by an evaluation relation whose reflexive-transitive closure is an Evaluation Preorder. Pairwise inconsistency over a chosen simplicial carrier gives a finite cochain complex, quotient residual space, and descended closure map. The core diagnostic is the obstruction signature (Φ₁, Γ₂, R_{cl}): Φ₁ measures quotient residual mass, Γ₂ measures d₁ closure charge, and R_{cl} records their ratio. Metric magnitude is not universal; it is selected by the observer's scalar gauges, aggregation law, and compatible transformation monoid. Sections §1.0–§1.10 establish the finite scalar core; Sections §2.0–§2.4 develop explicit finite extensions including arbitrary-degree simplicial cohomology, discrete mathematical physics and combinatorial conservation laws, and finite quantum trace-norm calculus with observer passivity. Why a Researcher Should Care Finite evaluation systems often produce local comparisons that cannot be globally reconciled — constraint solvers, distributed logs, model-evaluation traces, sensor networks, proof-search attempts, and multi-agent review pipelines all have this shape. This paper gives a finite diagnostic for that failure: the quotient Q¹ = C¹ / im(d₀) separates inconsistency removable by local reference changes from irreducible residual obstruction, while κ¹([h]) = d₁ h separates closed residual obstruction from active closure failure. The payoff is a replayable three-way classification of any observed inconsistency — removable gauge, closed obstruction, or non-closed rupture. System Architecture The paper integrates an exact discrete rational solver in Python with 9 sorry-free Lean 4 formalization modules: A. Lean 4 Formalization Layer (primitive_axiomatics in lean4) Core.lean: Root aggregation module and formal exports TriangleReplay.lean: Worked cyclic 2-simplex example replay KappaWellDefined.lean: Descended closure map κ¹ well-defined on quotient space Q¹ = C¹ / im(d₀) ExactSequence.lean: Short exact sequence 0 → H¹(P) → Q¹(P) → im(d₁) → 0 ClosureRatioBound.lean: Exact operator norm bound R_cl ≤ ‖d₁‖₁→₁ ObserverPassivity.lean: Observer non-creation inequality Φ_O(O(q)) ≤ Φ(q) ObserverFamilyPoset.lean: Observer poset and refinement structure GrammarBound.lean: Finite observer resolution and vocabulary bound |Q¹_G| ≤ |im(r)| ≤ |G| ConstructorIncrement.lean: Minimal increment initiality boundary and inductive preservation B. Exact Rational Python Replay Engine (code/l000_replay.py) Implemented strictly in pure Python standard library (`fractions.Fraction`) with zero floating-point approximation: Finite Complexes: Exact finite cochain spaces C⁰, C¹, C² Coboundaries: Boundary operators d₀, d₁ with verified nilpotence d₁ ∘ d₀ = 0 Primal Optimization: Exact ℓ¹ quotient residual minimization (Φ₁ = 2) Dual Certificate: Exact dual witness verification (d₀* ψ = 0, ‖ψ‖_∞ ≤ 1, ⟨ψ, δ⟩ = Φ₁ = 2) Zero Duality Gap: Primal optimum matches the dual witness certificate over ℚ Closure Invariants: Direct evaluation of closure charge Γ₂ = 2 and closure ratio R_cl = 1 C. Test Suite & Verification Test Suite (code/test_l000_replay.py): 81 unit test cases passing with 99% branch coverage (verifying nilpotency, optimality, dual witnesses, zero gap, and gauge invariance) Reviewer Notebook (jupyter_notebooks/001_reviewer_primitive_axiomatics.ipynb): Interactive inspection sandbox with headless launch scripts (`public_export/run_notebook.bat` / `.sh`) Key Closed Forms & Formulations Quotient Residual Magnitude & Dual Certificate: Φ₁([δ]) = inf { ‖δ - d₀ f‖₁ : f ∈ C⁰ } = max { ⟨ψ, δ⟩ : ‖ψ‖_∞ ≤ 1, d₀* ψ = 0, ψ ∈ C¹ } Closure Charge: Γ₂(δ) = ‖d₁ δ‖₁ Descended Closure Map: κ¹([h]) = d₁ h ∈ im(d₁), well-defined on Q¹ = C¹ / im(d₀) Closure Ratio Bound: 0 ≤ R_{cl}([h]) = Γ₂(h) / Φ₁([h]) ≤ ‖d₁‖_{1→1} Exact Sequence: 0 → H¹(P) → Q¹(P) →(κ¹) im(d₁) → 0 Observer Passivity (No-Creation): Φ_O(O(q)) ≤ Φ(q) Observer Grammar Resolution Bound: |Q¹_G| ≤ |im(r)| ≤ |G| ≤ ∑_{ℓ ≤ L} |Σ|^ℓ Negative Scopes & Non-Claims No derivation of quantum mechanics, Hilbert spaces, or the Born rule from Φ₁. No Lorentz invariance, spacetime relativity, or physical gauge coupling constants. No universal claim that metric geometry is fundamentally ℓ¹; ℓ¹ is strictly conditional on observer symmetry and replica-extensivity axioms. No autonomous promotion, moral authority, or legal certificate conferred by (Φ₁, Γ₂, R_{cl}) alone. See `docs/nonclaims.md` for complete scope fences. Cold Reproduction & Verification Python Tests: python -m unittest discover -s code -p "test_*.py" (81 passed; statement coverage >= 99%). Lean 4 Build: cd lean4 && lake build (all 9 modules sorry-free; standard kernel axioms only). Notebook Launcher: public_export/run_notebook.bat or public_export/run_notebook.sh. Publication PDF: Source-buildable and content-equivalent via python scripts/build_paper_artifacts.py. The submitted primitive_axiomatics.pdf (SHA-256 bound in SHA256SUMS) is the authoritative publication rendering.

Zenodo (CERN European Organization for Nuclear Research)
Life in Land
Logic, Reasoning, and Knowledge
AI Navigator

Ask Laika to Summarize, Analyze, and Connect papers live on the map.

Summarize Papers & Methodologies

Extract key findings, datasets, and comparative methods across publications.

Benchmark Rankings & Visual Analytics

Rank top research institutions, authors, funders, topics, and journals by Field-Weighted Citation Impact (FWCI) and paper volume with instant charts.

Connect Distant Disciplines

Bridge topological clusters on the map to find hidden collaborative intersections.